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
G : Type u_5
inst✝¹³ : AddCommGroup E✝
inst✝¹² : Module 𝕜₁ E✝
inst✝¹¹ : TopologicalSpace E✝
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜₂ F✝
𝕜 : Type u_6
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
⊢ Continuous[Pi.topologicalSpace, UniformOnFun.topologicalSpace E ((i : ι) → F i) 𝔖]
    ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) ∘ fun F_1 ↦ ContinuousLinearMap.pi F_1)

Tactic:
rw [UniformOnFun.uniformEquivPiComm _ _ |>.isUniformEmbedding.isEmbedding.continuous_iff]

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁵ : NormedField 𝕜₁
inst✝¹⁴ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E✝ : Type u_3
F✝ : Type u_4
G : Type u_5
inst✝¹³ : AddCommGroup E✝
inst✝¹² : Module 𝕜₁ E✝
inst✝¹¹ : TopologicalSpace E✝
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜₂ F✝
𝕜 : Type u_6
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
⊢ Continuous[Pi.topologicalSpace, (Pi.uniformSpace fun i ↦ E →ᵤ[𝔖] F i).toTopologicalSpace]
    (⇑(UniformOnFun.uniformEquivPiComm 𝔖 F) ∘
      (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) ∘ fun F_1 ↦ ContinuousLinearMap.pi F_1)
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup F
inst✝⁷ : SeminormedAddCommGroup G
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₂] F
g : E →SL[σ₁₃] G
h : ∀ (x : E), ‖f x‖ = ‖g x‖
x : E
⊢ ‖f x‖ ≤ ‖g‖ * ‖x‖

Tactic:
rw [h x]
      exact le_opNorm _ _

Goal state after:
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
G : Type u_5
inst✝¹³ : AddCommGroup E✝
inst✝¹² : Module 𝕜₁ E✝
inst✝¹¹ : TopologicalSpace E✝
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜₂ F✝
𝕜 : Type u_6
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
⊢ Continuous[Pi.topologicalSpace, instTopologicalSpace (RingHom.id 𝕜) ((i : ι) → F i) 𝔖] fun F_1 ↦
    ContinuousLinearMap.pi F_1

Tactic:
by
      rw [UniformConvergenceCLM.isEmbedding_coeFn _ _ _ |>.continuous_iff]
      rw [UniformOnFun.uniformEquivPiComm _ _ |>.isUniformEmbedding.isEmbedding.continuous_iff]
      refine continuous_pi fun i ↦ ?_
      exact UniformConvergenceCLM.isEmbedding_coeFn _ _ _ |>.continuous.comp (continuous_apply i)

Goal state after:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : μ s ≠ ∞
t : Set Ω
⊢ μ[t | s] * μ s = μ (s ∩ t)

Tactic:
obtain hcs | hcs := eq_or_ne (μ s) 0

Goal state after:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : μ s ≠ ∞
t : Set Ω
hcs : μ s = 0
⊢ μ[t | s] * μ s = μ (s ∩ t)

case inr
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : μ s ≠ ∞
t : Set Ω
hcs : μ s ≠ 0
⊢ μ[t | s] * μ s = μ (s ∩ t)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : (i : ι) → MetricSpace (α i)
x : (i : ι) → α i
r : ℝ
hr : 0 ≤ r
⊢ (Measure.pi μ) (Metric.closedBall x r) = ∏ i, (μ i) (Metric.closedBall (x i) r)

Tactic:
closedBall_pi _ hr,

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : (i : ι) → MetricSpace (α i)
x : (i : ι) → α i
r : ℝ
hr : 0 ≤ r
⊢ (Measure.pi μ) (univ.pi fun b ↦ Metric.closedBall (x b) r) = ∏ i, (μ i) (Metric.closedBall (x i) r)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ (Measure.pi μ) ((fun f ↦ f i) ⁻¹' s) = ((∏ j ∈ Finset.univ.erase i, (μ j) univ) • μ i) s

Tactic:
← Set.univ_pi_update_univ,

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ (Measure.pi μ) (univ.pi (update (fun j ↦ univ) i s)) = ((∏ j ∈ Finset.univ.erase i, (μ j) univ) • μ i) s
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : p = ∞
⊢ essSup (fun x ↦ s.indicator (fun a ↦ ‖f a‖ₑ) x) μ = essSup (fun a ↦ ‖f a‖ₑ) (μ.restrict s)

Tactic:
ENNReal.essSup_indicator_eq_essSup_restrict hs

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : Fintype ι'
f : ι' ≃ ι
s : (i : ι) → Set (α i)
x✝ : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.pi fun i' ↦ μ (f i')) (⇑(Equiv.piCongrLeft α f) ⁻¹' univ.pi s) = ∏ i, (μ i) (s i)

Tactic:
Equiv.piCongrLeft_preimage_univ_pi,

Goal state after:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : Fintype ι'
f : ι' ≃ ι
s : (i : ι) → Set (α i)
x✝ : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.pi fun i' ↦ μ (f i')) (univ.pi fun i ↦ s (f i)) = ∏ i, (μ i) (s i)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case pos
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

Tactic:
simp [h_top, eLpNormEssSup_eq_essSup_enorm]

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

Goal state before:
pp: case mp
α : Type u_7
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
h : a ≤ b * c
⊢ a = 0 ∧ c = 0

Tactic:
exact
      ⟨(h.trans (mul_nonpos_of_nonpos_of_nonneg hb.le hc)).antisymm ha,
        (nonpos_of_mul_nonneg_right (ha.trans h) hb).antisymm hc⟩

Goal state after:
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
⊢ 1 / p + 1 / q = 1 / r

Tactic:
by simpa using inv_add_inv_eq_inv ..

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ rexp y - rexp x < rexp y * (y - x)

Tactic:
calc
      exp y - exp x = exp y - exp y * exp (x - y) := by rw [← exp_add]; ring_nf
      _ = exp y * (1 - exp (x - y)) := by ring
      _ < exp y * -(x - y) := by gcongr; linarith [add_one_lt_exp h2.ne]
      _ = exp y * (y - x) := by ring

Goal state after:
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ q ≠ 1 ↔ 1 < q

Tactic:
ne_comm,

Goal state after:
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ 1 ≠ q ↔ 1 < q
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
f : α → ε
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun a ↦ ‖f a‖ₑ ^ q) =ᵐ[μ] 0 ∧ 0 < q
⊢ f =ᵐ[μ] 0

Tactic:
refine h.left.mono fun x hx ↦ ?_

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
f : α → ε
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun a ↦ ‖f a‖ₑ ^ q) =ᵐ[μ] 0 ∧ 0 < q
x : α
hx : (fun a ↦ ‖f a‖ₑ ^ q) x = 0 x
⊢ f x = 0 x
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inl
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
h₀ : w i = 0
⊢ z i ^ w i = x ^ w i

pp: case inr
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
h₀ : w i ≠ 0
⊢ z i ^ w i = x ^ w i

Tactic:
· rw [h₀, rpow_zero, rpow_zero]

Goal state after:
case inr
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
h₀ : w i ≠ 0
⊢ z i ^ w i = x ^ w i
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case e'_4
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p

Tactic:
· simp only [mul_rpow_of_nonneg _ _ (zero_le_one.trans hp), rpow_sub _ _ two_ne_zero ofNat_ne_top,
      ENNReal.div_eq_inv_mul, rpow_one, mul_one]
    ring

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)
ε : ℝ≥0∞
⊢ 0 < ε → Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
hε

Goal state after:
α : 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)
ε : ℝ≥0∞
hε : 0 < ε
⊢ Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
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
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
⊢ 0 < ε → Tendsto (fun i ↦ μ {x | ε ≤ edist (f' i x) (g' x)}) l (𝓝 0)

Tactic:
hε

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
⊢ Tendsto (fun i ↦ μ {x | ε ≤ edist (f' i x) (g' x)}) l (𝓝 0)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
hf_sum : Summable fun i ↦ f i ^ p
hg_sum : Summable fun i ↦ g i ^ q
⊢ (Summable fun i ↦ (f i * g i) ^ r) ∧
    ∑' (i : ι), (f i * g i) ^ r ≤ (∑' (i : ι), f i ^ p) ^ (r / p) * (∑' (i : ι), g i ^ q) ^ (r / q)

Tactic:
by
  lift f to ι → ℝ≥0 using hf
  lift g to ι → ℝ≥0 using hg
  -- After https://github.com/leanprover/lean4/pull/2734, `norm_cast` needs help with beta reduction.
  beta_reduce at *
  norm_cast at *
  exact NNReal.summable_and_Lr_rpow_le_Lp_mul_Lq_tsum hpqr hf_sum hg_sum

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
f g : ↥(Lp E p μ)
⊢ dist f g = (eLpNorm (↑↑f - ↑↑g) p μ).toReal

Tactic:
by
  rw [dist_eq_eLpNorm_neg_add, ← eLpNorm_neg, neg_add, neg_neg, sub_eq_add_neg]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
hp : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
this : ‖f + g‖ₑ ≤ ‖f‖ₑ + ‖g‖ₑ
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
simpa only [ge_iff_le, enorm, ← ENNReal.coe_add, ENNReal.coe_le_coe] using! this

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

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k ↦ {x | 2⁻¹ ^ k ≤ edist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : μ s = 0
x : α
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
hNx : ∀ i ≥ N, edist (f (ns i) x) (g x) < 2⁻¹ ^ i
k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hn_ge : n ≥ max N (k - 1)
⊢ edist (f (ns n) x) (g x) ≤ 2 * 2⁻¹ ^ k

Tactic:
specialize hNx n ((le_max_left _ _).trans hn_ge)

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k ↦ {x | 2⁻¹ ^ k ≤ edist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : μ s = 0
x : α
ε : ℝ≥0∞
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hNx : edist (f (ns n) x) (g x) < 2⁻¹ ^ n
hn_ge : n ≥ max N (k - 1)
⊢ edist (f (ns n) x) (g x) ≤ 2 * 2⁻¹ ^ k
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
f : α → E
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp (fun x ↦ ‖f x‖ ^ p.toReal) 1 μ

Tactic:
convert! hf.norm_rpow_div p

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ 1 = p / p
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: p : ℝ≥0∞
α : Type u_6
E : Type u_7
F : Type u_8
K' : ℝ≥0
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : α → E
g : E → F
hL : MemLp (g ∘ f) p μ
hg : UniformContinuous g
hg' : AntilipschitzWith K' g
g0 : g 0 = 0
⊢ MemLp f p μ

Tactic:
have A : ∀ x, ‖f x‖ ≤ K' * ‖g (f x)‖ := by
    intro x
    -- TODO: add `AntilipschitzWith.le_mul_nnnorm_sub` and `AntilipschitzWith.le_mul_norm`
    rw [← dist_zero_right, ← dist_zero_right, ← g0]
    apply hg'.le_mul_dist

Goal state after:
p : ℝ≥0∞
α : Type u_6
E : Type u_7
F : Type u_8
K' : ℝ≥0
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : α → E
g : E → F
hL : MemLp (g ∘ f) p μ
hg : UniformContinuous g
hg' : AntilipschitzWith K' g
g0 : g 0 = 0
A : ∀ (x : α), ‖f x‖ ≤ ↑K' * ‖g (f x)‖
⊢ MemLp f 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✝² : Lattice E
inst✝¹ : HasSolidNorm E
inst✝ : IsOrderedAddMonoid E
f g : α →ₘ[μ] E
hf : MemLp (↑f) p μ
hg : MemLp (↑g) p μ
⊢ MemLp (↑(f ⊔ g)) p μ

Tactic:
exact (memLp_congr_ae (AEEqFun.coeFn_sup _ _)).mpr (hf.sup hg)

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
inst✝¹ : NormedSpace ℝ E
ν : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ≤ c • ν
inst✝ : Fact (1 ≤ p)
f : ↥(Lp E p ν)
⊢ eLpNorm (↑↑f) p μ ≤ c ^ (1 / p).toReal * eLpNorm (↑↑f) p ν

Tactic:
exact eLpNorm_le_of_measure_le_smul h

Goal state after:
Module: Mathlib.Data.Fintype.CardEmbedding

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : ‖α₁ ↪ β‖ = ‖β‖.descFactorial ‖α₁‖
⊢ ‖α₂ ↪ β‖ = ‖β‖.descFactorial ‖α₂‖

Tactic:
clear! α

Goal state after:
case refine_1
β : Type u_2
inst✝ : Fintype β
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : ‖α₁ ↪ β‖ = ‖β‖.descFactorial ‖α₁‖
⊢ ‖α₂ ↪ β‖ = ‖β‖.descFactorial ‖α₂‖
Module: Mathlib.Data.Fintype.CardEmbedding

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
⊢ ‖PEmpty.{u_1 + 1} ↪ β‖ = ‖β‖.descFactorial ‖PEmpty.{u_1 + 1}‖

Tactic:
clear! α

Goal state after:
case refine_2
β : Type u_2
inst✝ : Fintype β
⊢ ‖PEmpty.{u_1 + 1} ↪ β‖ = ‖β‖.descFactorial ‖PEmpty.{u_1 + 1}‖
Module: Mathlib.Data.Fintype.CardEmbedding

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
⊢ ‖Option γ ↪ β‖ = ‖β‖.descFactorial ‖Option γ‖

Tactic:
clear! α

Goal state after:
case refine_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
⊢ ‖Option γ ↪ β‖ = ‖β‖.descFactorial ‖Option γ‖
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
hp_top : ¬p = ∞
hp1 : 1 ≤ p.toReal
N : ℕ
⊢ ∀ (n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p.toReal μ < B N

Tactic:
n

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
hp_top : ¬p = ∞
hp1 : 1 ≤ p.toReal
N n : ℕ
⊢ ∀ (m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p.toReal μ < B N
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ≥0∞
hδ : 0 < δ
hδ_top : δ ≠ ∞
hfg : ∀ ε > 0, ∀ᶠ (x : ι) in l, essSup (fun x_1 ↦ ‖(f x - g) x_1‖ₑ) μ ≤ ε
ε : ℝ≥0∞
⊢ ε > 0 → ∀ᶠ (x : ι) in l, μ {x_1 | δ ≤ edist (f x x_1) (g x_1)} ≤ ε

Tactic:
hε

Goal state after:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ≥0∞
hδ : 0 < δ
hδ_top : δ ≠ ∞
hfg : ∀ ε > 0, ∀ᶠ (x : ι) in l, essSup (fun x_1 ↦ ‖(f x - g) x_1‖ₑ) μ ≤ ε
ε : ℝ≥0∞
hε : ε > 0
⊢ ∀ᶠ (x : ι) in l, μ {x_1 | δ ≤ edist (f x x_1) (g x_1)} ≤ ε
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
⊢ ε > 0 → ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε

Tactic:
hε

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
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
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
⊢ ‖0‖ = 0

Tactic:
exact opNorm_zero

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

Goal state before:
pp: case inr
𝕜 : 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 = 1 ∧ ‖x‖ < 1
⊢ C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖

Tactic:
hx.1,

Goal state after:
case inr
𝕜 : 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 = 1 ∧ ‖x‖ < 1
⊢ C * ‖x‖ * ‖y‖ ≤ C * 1 * ‖y‖
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: case refine_1
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
⊢ 0 < ε → Metric.closedBall 0 ε ∈ 𝓝 0

Tactic:
hε

Goal state after:
case refine_1
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
⊢ Metric.closedBall 0 ε ∈ 𝓝 0
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 : α → ε
h : μ = 0
⊢ Integrable f ((μ univ)⁻¹ • μ) ↔ Integrable f μ

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : 0 ≤ᵐ[μ] f
hg : 0 ≤ᵐ[μ] g
h_int : Integrable (f + g) μ
a : α
haf : 0 a ≤ f a
hag : 0 a ≤ g a
⊢ ‖f a‖ ≤ (f + g) a

Tactic:
exact (Real.norm_of_nonneg haf).symm ▸ le_add_of_nonneg_right hag

Goal state after: