mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F✝ : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F✝
inst✝⁶ : Module 𝕜₂ F✝
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
hF : T2Space F
H₁ :
  IsClosed[UniformOnFun.topologicalSpace E F 𝔖]
    {f | Continuous[inst✝⁸, inst✝³.toTopologicalSpace] ((UniformOnFun.toFun 𝔖) f)}
⊢ IsClosed[(UniformOnFun.uniformSpace E F 𝔖).toTopologicalSpace] (range (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe))

Tactic:
convert!
    H₁.inter <|
      (LinearMap.isClosed_range_coe E F σ).preimage
        (UniformOnFun.uniformContinuous_toFun h𝔖U).continuous

Goal state after:
case e'_3
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F✝ : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F✝
inst✝⁶ : Module 𝕜₂ F✝
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
hF : T2Space F
H₁ :
  IsClosed[UniformOnFun.topologicalSpace E F 𝔖]
    {f | Continuous[inst✝⁸, inst✝³.toTopologicalSpace] ((UniformOnFun.toFun 𝔖) f)}
⊢ range (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) =
    {f | Continuous[inst✝⁸, inst✝³.toTopologicalSpace] ((UniformOnFun.toFun 𝔖) f)} ∩
      ⇑(UniformOnFun.toFun 𝔖) ⁻¹' range DFunLike.coe
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜₂ F
𝕜₁ : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup G
𝕜₃ : Type u_7
inst✝⁸ : NormedField 𝕜₃
inst✝⁷ : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst✝⁶ : RingHomSurjective τ
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousConstSMul 𝕜₂ F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] E →SLᵤ[σ, 𝔖] F
hB : Continuous[instTopologicalSpaceProd, inst✝⁵] fun p ↦ (B p.1) p.2
this : ∀ s ∈ 𝔖, ∀ U ∈ 𝓝 0, ∀ᶠ (g : G) in 𝓝 0, ∀ e ∈ s, (B g) e ∈ U
⊢ Tendsto (⇑B) (𝓝 0) (𝓝 0)

Tactic:
simpa [UniformConvergenceCLM.nhds_zero_eq, MapsTo]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)
⊢ ‖-f.1 + f.2‖ = ‖f.1 - f.2‖

Tactic:
rw [← opNorm_neg, neg_add, neg_neg, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h✝ : α → β
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : ExistsMulOfLE β
x y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
⊢ ∃ c, ↑g = ↑f * c

Tactic:
by
    classical
    choose c hc using fun x (hx : f x ≤ g x) ↦ exists_mul_of_le hx
    refine ⟨ofFun fun x ↦ if hx : f x ≤ g x then c x hx else f x, coe_eq.2 ?_⟩
    filter_upwards [h] with x hx
    rw [dif_pos hx, hc]

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ Continuous[instTopologicalSpace, inst✝] ⇑(CompactCoherentification.mk X).symm

Tactic:
rw [continuous_dom_iff]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ ∀ (K : Set X), IsCompact K → ContinuousOn (⇑(CompactCoherentification.mk X).symm ∘ ⇑(CompactCoherentification.mk X)) K
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : ∀ (K : Set X), IsCompact K → ContinuousOn f K
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (CompactCoherentification.map f)

Tactic:
simp_rw [continuous_dom_iff, CompactCoherentification.map_comp_mk]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : ∀ (K : Set X), IsCompact K → ContinuousOn f K
⊢ ∀ (K : Set X), IsCompact K → ContinuousOn (⇑(CompactCoherentification.mk Y) ∘ f) K
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
⊢ μ[|∅] = 0

Tactic:
by simp [cond]

Goal state after:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
⊢ μ[|s] = 0 ↔ μ s = ∞ ∨ μ s = 0

Tactic:
by simp [cond]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : IsEmpty ι
⊢ piPremeasure m (univ.pi s) = ∏ i, (m i) (s i)

Tactic:
simp [piPremeasure]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: α : Type u_4
inst✝¹ : Fintype α
inst✝ : IsEmpty α
β : α → Type u_5
m : (α : α) → MeasurableSpace (β α)
μ : (a : α) → Measure (β a)
⊢ (Measure.pi μ) univ = 1

Tactic:
by
  rw [pi_of_empty, measure_univ]

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case refine_1
w₁ w₂ z₁ z₂ : ℝ≥0
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i, ![w₁, w₂] i = 1

Tactic:
· simp [hw', Fin.sum_univ_succ]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
⊢ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

Tactic:
have hz' := fun i h => lt_of_le_of_ne (hz i h) (fun a => (ne_of_gt (hw i h)) (A i h a.symm))

Goal state after:
case neg
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
⊢ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : (∑ i ∈ s, w i * z i) ^ p ≠ ∞
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
i : ι
hi : i ∈ s
⊢ w i * z i ^ p ≠ ∞

Tactic:
specialize h_top i hi

Goal state after:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : (∑ i ∈ s, w i * z i) ^ p ≠ ∞
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ∞
i : ι
h_top : w i * z i ≠ ∞
hi : i ∈ s
⊢ w i * z i ^ p ≠ ∞
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : ∑ i ∈ insert i₀ s, p i = 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
⊢ ∀ i ∈ s, p i = 0

Tactic:
simpa [hi₀, h2i₀, sum_eq_zero_iff_of_nonneg (fun i hi ↦ h2p i <| mem_insert_of_mem hi)]
          using hp

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case refine_1
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i, ![w₁, w₂] i = 1

Tactic:
· simp [hw', Fin.sum_univ_succ]

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case pos
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
hmem : (ENNReal.ofReal p)⁻¹ ∈ Set.Ioo 0 1
⊢ (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)

Tactic:
exact rpow_add_le_mul_rpow_add_rpow _ _ h.le

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ 0 ≤ 1 / p - 1 / q

Tactic:
le_sub_comm,

Goal state after:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ 1 / q ≤ 1 / p - 0
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ∞
hpq : p ≤ q
⊢ Function.support f ⊆ toMeasurable μ s

Tactic:
apply Function.support_subset_iff'.2 fun x hx ↦ hf x ?_

Goal state after:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ∞
hpq : p ≤ q
x : α
hx : x ∉ toMeasurable μ s
⊢ x ∉ s
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr : p.HolderTriple q r
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f p μ * eLpNorm g q μ

Tactic:
have hpqr := hpqr.one_div_eq
  obtain (rfl | rfl | hp) := ENNReal.trichotomy p
  · simp_all
  · have : r = q := by simpa using hpqr
    exact this ▸ eLpNorm_le_eLpNorm_top_mul_eLpNorm r f hg b c h
  obtain (rfl | rfl | hq) := ENNReal.trichotomy q
  · simp_all
  · have : r = p := by simpa using hpqr
    exact this ▸ eLpNorm_le_eLpNorm_mul_eLpNorm_top p hf g b c h
  obtain ⟨hp₁, hp₂⟩ := ENNReal.toReal_pos_iff.mp hp
  obtain ⟨hq₁, hq₂⟩ := ENNReal.toReal_pos_iff.mp hq
  have hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal := by
    have := congr(ENNReal.toReal $(hpqr))
    rw [ENNReal.toReal_add (by simpa using hp₁.ne') (by simpa using hq₁.ne')] at this
    simpa
  have hr : 0 < r.toReal := one_div_pos.mp <| by rw [hpqr']; positivity
  obtain ⟨hr₁, hr₂⟩ := ENNReal.toReal_pos_iff.mp hr
  have hrp : r.toReal < p.toReal := lt_of_one_div_lt_one_div hp <|
    hpqr' ▸ lt_add_of_pos_right _ (by positivity)
  rw [eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm']
  · exact eLpNorm'_le_eLpNorm'_mul_eLpNorm' hf hg b c h hr hrp hpqr'
  all_goals first | positivity | finiteness

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✝¹ : PseudoMetricSpace E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
⊢ TendstoInMeasure μ f l g ↔ ∀ (ε : ℝ), 0 < ε → Tendsto (fun i ↦ μ.real {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)

Tactic:
by
  rw [tendstoInMeasure_iff_dist]
  congr! with ε hε hε_top
  simp_rw [measureReal_def, ENNReal.tendsto_toReal_zero_iff (fun _ ↦ measure_ne_top _ _)]

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

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

Tactic:
have hf : (fun i => (μ { x | ε ≤ edist (f i x) (g x) }).toNNReal) =
        ENNReal.toNNReal ∘ (fun i ↦ (μ { x | ε ≤ edist (f i x) (g x) })) := rfl
    rw [hf, ENNReal.tendsto_toNNReal_iff' (hfin ε)]
    exact h ε hε

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
⊢ (fun a ↦ ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p) = fun a ↦
    (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p

Tactic:
ext1 a

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p = (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
h_is_o : (fun t ↦ (↑x + t)⁻¹ʳ - ↑x⁻¹) =o[𝓝 0] fun x ↦ 1
h_lim : Tendsto (fun y ↦ y - ↑x) (𝓝 ↑x) (𝓝 0)
⊢ Tendsto (fun e ↦ ‖e⁻¹ʳ - (↑x)⁻¹ʳ‖) (𝓝 ↑x) (𝓝 0)

Tactic:
inverse_unit

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
h_is_o : (fun t ↦ (↑x + t)⁻¹ʳ - ↑x⁻¹) =o[𝓝 0] fun x ↦ 1
h_lim : Tendsto (fun y ↦ y - ↑x) (𝓝 ↑x) (𝓝 0)
⊢ Tendsto (fun e ↦ ‖e⁻¹ʳ - ↑x⁻¹‖) (𝓝 ↑x) (𝓝 0)
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: case inl
𝕜 : 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
x : E
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
y : F
hx : max ‖x‖ 1 = ‖x‖ ∧ 1 ≤ ‖x‖
⊢ C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖

Tactic:
grw [hx.1]

Goal state after:
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
x : E
⊢ ∃ M, 0 < M ∧ ∀ (x_1 : F), ‖f (x, x_1)‖ ≤ M * ‖x_1‖

Tactic:
let ⟨C, hC_pos, hC⟩ := h.bound
    -- Using `C * ‖x‖` is tempting but `x` might be 0 and the constant must be positive!
    refine ⟨C * max ‖x‖ 1, by positivity, fun y ↦ (hC x y).trans ?_⟩
    rcases max_cases ‖x‖ 1 with hx | hx
    · grw [hx.1]
    · grw [hx.1, hx.2.le]

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 : α → E
⊢ AEStronglyMeasurable g (μ.withDensity fun x ↦ ↑(f x)) → AEStronglyMeasurable (fun x ↦ ↑(f x) • g x) μ

Tactic:
rintro ⟨g', g'meas, hg'⟩

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'
⊢ AEStronglyMeasurable (fun x ↦ ↑(f x) • g x) μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Goal state before:
pp: case mpr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEStronglyMeasurable (fun x ↦ ↑(f x) • g x) μ → AEStronglyMeasurable g (μ.withDensity fun x ↦ ↑(f x))

Tactic:
rintro ⟨g', g'meas, hg'⟩

Goal state after:
case mpr
α : 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' : (fun x ↦ ↑(f x) • g x) =ᵐ[μ] g'
⊢ AEStronglyMeasurable g (μ.withDensity fun x ↦ ↑(f x))
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✝ : ContinuousSub M
h : IsTopCompl p q
⊢ Continuous[inst✝³, inst✝³] ⇑(q.projection p ⋯)

Tactic:
rw [projection_eq_id_sub_projection h.isCompl]

Goal state after:
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✝ : ContinuousSub M
h : IsTopCompl p q
⊢ Continuous[inst✝³, inst✝³] ⇑(LinearMap.id - p.projection q ⋯)
Module: Mathlib.MeasureTheory.Measure.Real

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

Tactic:
rw [union_comm]
  exact measureReal_le_measureReal_union_left h

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
⊢ (fun x ↦ ENNReal.ofReal (f x).toReal) =ᵐ[μ] f

Tactic:
filter_upwards [hf]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
⊢ ∀ (a : α), f a < ∞ → ENNReal.ofReal (f a).toReal = f a
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
⊢ (fun x ↦ ↑(f x).toNNReal) =ᵐ[μ] f

Tactic:
filter_upwards [hf]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
⊢ ∀ (a : α), f a < ∞ → ↑(f a).toNNReal = f a
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

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

Tactic:
intro hs

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x ↦ ‖f x‖
⊢ AEStronglyMeasurable f Measure.count
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
l : Filter α
inst✝ : l.IsMeasurablyGenerated
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ f)
⊢ IntegrableAtFilter f l μ

Tactic:
by
  obtain ⟨C, hC⟩ : ∃ C, ∀ᶠ s in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C :=
    hf.imp fun C hC => eventually_smallSets.2 ⟨_, hC, fun t => id⟩
  rcases (hfm.eventually.and (hμ.eventually.and hC)).exists_measurable_mem_of_smallSets with
    ⟨s, hsl, hsm, hfm, hμ, hC⟩
  refine ⟨s, hsl, ⟨hfm, .restrict_of_bounded hμ (C := C) ?_⟩⟩
  rw [ae_restrict_eq hsm, eventually_inf_principal]
  exact Eventually.of_forall hC

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

Goal state before:
pp: 𝕜 : 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
⊢ ‖(f.restr s hk z) v‖ ≤ C * ‖z‖ ^ (n - k) * ∏ i, ‖v i‖

Tactic:
rw [mul_right_comm, mul_assoc]

Goal state after:
𝕜 : 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
⊢ ‖(f.restr s hk z) v‖ ≤ C * ((∏ i, ‖v i‖) * ‖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 × ContinuousMultilinearMap 𝕜 E G
⊢ ‖-f.1 + f.2‖ = ‖f.1 - f.2‖

Tactic:
rw [← opNorm_neg, neg_add, neg_neg, sub_eq_add_neg]

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

Goal state before:
pp: case h1
𝕜 : 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‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
f : ContinuousMultilinearMap 𝕜 E G
hf : ∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → ‖f x‖ ≤ 1
x : (i : ι) → E i
hcx : ∀ (i : ι), ‖c‖ / ‖c‖ ≤ ‖x i‖
hx : ∀ (i : ι), ‖x i‖ < ‖c‖
i : ι
a✝ : i ∈ univ
⊢ 1 ≤ ‖x i‖

Tactic:
simpa only [div_self hc₀.ne'] using hcx i

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

Goal state before:
pp: 𝕜 : 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 : G [×n]→L[𝕜] G'
s : Finset (Fin n)
hk : #s = k
z : G
⊢ ‖f.restr s hk z‖ ≤ ‖f‖ * ‖z‖ ^ (n - k)

Tactic:
by
  apply MultilinearMap.mkContinuous_norm_le
  exact mul_nonneg (norm_nonneg _) (pow_nonneg (norm_nonneg _) _)

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

Goal state before:
pp: ι : 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
inst✝ : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
this✝³ : MeasurableSpace E := ⋯
this✝² : BorelSpace E
this✝¹ : UpgradedIsCompletelyPseudoMetrizableSpace E := ⋯
s : Set E := ⋯
this✝ : SecondCountableTopology ↑s
this : IsCompletelyPseudoMetrizableSpace ↑s
g : ι → X → ↑s := ⋯
mg : ∀ (i : ι), Measurable (g i)
x : X
⊢ (∃ c, Tendsto (fun x_1 ↦ f x_1 x) l (𝓝 c)) ↔ ∃ c, Tendsto (fun n ↦ g n x) l (𝓝 c)

Tactic:
refine ⟨fun ⟨c, hc⟩ ↦ ⟨⟨c, ?_⟩, tendsto_subtype_rng.2 hc⟩,
    fun ⟨c, hc⟩ ↦ ⟨c, tendsto_subtype_rng.1 hc⟩⟩

Goal state after:
ι : 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
inst✝ : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
this✝³ : MeasurableSpace E := borel E
this✝² : BorelSpace E
this✝¹ : UpgradedIsCompletelyPseudoMetrizableSpace E := upgradeIsCompletelyPseudoMetrizable E
s : Set E := closure[inst✝³] (⋃ i, range (f i))
this✝ : SecondCountableTopology ↑s
this : IsCompletelyPseudoMetrizableSpace ↑s
g : ι → X → ↑s := fun i x ↦ ⟨f i x, ⋯⟩
mg : ∀ (i : ι), Measurable (g i)
x : X
x✝ : ∃ c, Tendsto (fun x_1 ↦ f x_1 x) l (𝓝 c)
c : E
hc : Tendsto (fun x_1 ↦ f x_1 x) l (𝓝 c)
⊢ c ∈ s