mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g | EqOn (⇑g) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
x : α
hx : x ∈ s
⊢ Inseparable (f x) (f' x)

Tactic:
refine tendsto_nhds_unique_inseparable ?_ ((continuous_eval_const x).continuousAt.mono_left hf')

Goal state after:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g | EqOn (⇑g) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
x : α
hx : x ∈ s
⊢ Tendsto (fun f ↦ f x) l (𝓝 (f x))
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : μ[t | s] ≠ 0
⊢ (μ s)⁻¹ * μ (s ∩ t) ≠ 0

Tactic:
convert! hcst

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : μ[t | s] ≠ 0
⊢ (μ s)⁻¹ * μ (s ∩ t) = μ[t | s]
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
this : univ.pi (update (fun i' ↦ iUnion (t i')) i (⋃ x, s)) = univ.pi fun k ↦ ⋃ j, update (fun i' ↦ t i' j) i s k
⊢ MeasurableSet (univ.pi fun k ↦ ⋃ j, update (fun i' ↦ t i' j) i s k)

Tactic:
← iUnion_univ_pi

Goal state after:
case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
this : univ.pi (update (fun i' ↦ iUnion (t i')) i (⋃ x, s)) = univ.pi fun k ↦ ⋃ j, update (fun i' ↦ t i' j) i s k
⊢ MeasurableSet (⋃ x, univ.pi fun a ↦ update (fun i' ↦ t i' (x a)) i s a)
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : f' ≤ f
hg : f' ≤ g
⊢ f' ≤ f ⊓ g

Tactic:
rw [← coeFn_le] at hf hg ⊢
  filter_upwards [hf, hg, coeFn_inf f g] with _ haf hag ha_inf
  rw [ha_inf]
  exact le_inf haf hag

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
⊢ MemLp f p 0

Tactic:
by
  simp [MemLp]

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

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

Tactic:
by
  constructor
  · intro h
    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⟩
  · rintro ⟨rfl, rfl⟩
    rw [mul_zero]

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

Goal state before:
pp: case mpr
p : ℝ≥0∞
inst✝ : p.HolderConjugate 1
⊢ p = ∞

Tactic:
rw [← inv_inv p, ← one_sub_inv 1 p]

Goal state after:
case mpr
p : ℝ≥0∞
inst✝ : p.HolderConjugate 1
⊢ (1 - 1⁻¹)⁻¹ = ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
⊢ eLpNormEssSup f (c • μ) = eLpNormEssSup f μ

Tactic:
simp_rw [eLpNormEssSup]; exact essSup_ennreal_smul_measure hc _

Goal state after:
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹

Tactic:
obtain rfl | hp₁ := hp.eq_or_lt

Goal state after:
case inl
hp : 1 ≤ 1
this : 1 ≠ 0
⊢ 1 + (1 - 1)⁻¹ = (1⁻¹ - 1⁻¹)⁻¹

case inr
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
⊢ 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
a : α
⊢ (f * g) a = (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg)

Tactic:
rw [Pi.mul_apply, fun_eq_funMulInvSnorm_mul_eLpNorm f hf_nonzero hf_nontop,
        fun_eq_funMulInvSnorm_mul_eLpNorm g hg_nonzero hg_nontop, Pi.mul_apply]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
a : α
⊢ funMulInvSnorm f p μ a * (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p) *
      (funMulInvSnorm g q μ a * (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)) =
    funMulInvSnorm f p μ a * funMulInvSnorm g q μ a * (npf * nqg)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: w₁ w₂ p₁ p₂ : ℝ
hw₁ : 0 ≤ w₁
hw₂ : 0 ≤ w₂
hp₁ : 0 ≤ p₁
hp₂ : 0 ≤ p₂
hw : w₁ + w₂ = 1
⊢ ↑(⟨w₁, hw₁⟩ + ⟨w₂, hw₂⟩) = ↑1

Tactic:
by assumption

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ
hw₁ : 0 ≤ w₁
hw₂ : 0 ≤ w₂
hw₃ : 0 ≤ w₃
hw₄ : 0 ≤ w₄
hp₁ : 0 ≤ p₁
hp₂ : 0 ≤ p₂
hp₃ : 0 ≤ p₃
hp₄ : 0 ≤ p₄
hw : w₁ + w₂ + w₃ + w₄ = 1
⊢ ↑(⟨w₁, hw₁⟩ + ⟨w₂, hw₂⟩ + ⟨w₃, hw₃⟩ + ⟨w₄, hw₄⟩) = ↑1

Tactic:
by assumption

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
⊢ eLpNorm (f - g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)

Tactic:
simpa only [sub_eq_add_neg, eLpNorm_neg] using eLpNorm_add_le' hf hg.neg p

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h0 : a ≠ 0 ∧ b ≠ 0
h : a ≠ ∞ ∧ b ≠ ∞
⊢ ↑(a.toNNReal * b.toNNReal) = ↑(a.toNNReal ^ p) / ENNReal.ofReal p + ↑(b.toNNReal ^ q) / ENNReal.ofReal q ↔
    ↑a.toNNReal = ∞ ∧ ↑b.toNNReal ≠ 0 ∨ ↑a.toNNReal ≠ 0 ∧ ↑b.toNNReal = ∞ ∨ ↑(a.toNNReal ^ p) = ↑(b.toNNReal ^ q)

Tactic:
← ofNNReal_toNNReal,

Goal state after:
case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h0 : a ≠ 0 ∧ b ≠ 0
h : a ≠ ∞ ∧ b ≠ ∞
⊢ ↑(a.toNNReal * b.toNNReal) = ↑(a.toNNReal ^ p) / ↑p.toNNReal + ↑(b.toNNReal ^ q) / ENNReal.ofReal q ↔
    ↑a.toNNReal = ∞ ∧ ↑b.toNNReal ≠ 0 ∨ ↑a.toNNReal ≠ 0 ∧ ↑b.toNNReal = ∞ ∨ ↑(a.toNNReal ^ p) = ↑(b.toNNReal ^ q)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h0 : a ≠ 0 ∧ b ≠ 0
h : a ≠ ∞ ∧ b ≠ ∞
⊢ ↑(a.toNNReal * b.toNNReal) = ↑(a.toNNReal ^ p) / ↑p.toNNReal + ↑(b.toNNReal ^ q) / ENNReal.ofReal q ↔
    ↑a.toNNReal = ∞ ∧ ↑b.toNNReal ≠ 0 ∨ ↑a.toNNReal ≠ 0 ∧ ↑b.toNNReal = ∞ ∨ ↑(a.toNNReal ^ p) = ↑(b.toNNReal ^ q)

Tactic:
← ofNNReal_toNNReal,

Goal state after:
case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h0 : a ≠ 0 ∧ b ≠ 0
h : a ≠ ∞ ∧ b ≠ ∞
⊢ ↑(a.toNNReal * b.toNNReal) = ↑(a.toNNReal ^ p) / ↑p.toNNReal + ↑(b.toNNReal ^ q) / ↑q.toNNReal ↔
    ↑a.toNNReal = ∞ ∧ ↑b.toNNReal ≠ 0 ∨ ↑a.toNNReal ≠ 0 ∧ ↑b.toNNReal = ∞ ∨ ↑(a.toNNReal ^ p) = ↑(b.toNNReal ^ q)
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 : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
⊢ (∫⁻ (a : α), ‖b (f a) (g a)‖ₑ ^ r ∂μ) ^ (1 / r) ≤ (∫⁻ (a : α), ‖↑c • ‖f a‖ * ‖g a‖‖ₑ ^ r ∂μ) ^ (1 / r)

Tactic:
gcongr ?_ ^ _

Goal state after:
case h₁
α : 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 : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
⊢ ∫⁻ (a : α), ‖b (f a) (g a)‖ₑ ^ r ∂μ ≤ ∫⁻ (a : α), ‖↑c • ‖f a‖ * ‖g a‖‖ₑ ^ r ∂μ
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
p : ℝ
hp : 1 ≤ p
f : ι → ℝ≥0
hf_sum : Summable fun i ↦ ↑(f i) ^ p
g : ι → ℝ≥0
hg_sum : Summable fun i ↦ ↑(g i) ^ p
⊢ (Summable fun i ↦ (↑(f i) + ↑(g i)) ^ p) ∧
    (∑' (i : ι), (↑(f i) + ↑(g i)) ^ p) ^ (1 / p) ≤
      (∑' (i : ι), ↑(f i) ^ p) ^ (1 / p) + (∑' (i : ι), ↑(g i) ^ p) ^ (1 / p)

Tactic:
norm_cast0 at *

Goal state after:
ι : Type u
p : ℝ
f g : ι → ℝ≥0
hp : 1 ≤ p
hf_sum : Summable fun a ↦ f a ^ p
hg_sum : Summable fun a ↦ g a ^ p
⊢ (Summable fun a ↦ (f a + g a) ^ p) ∧
    (∑' (a : ι), (f a + g a) ^ p) ^ (1 / p) ≤ (∑' (a : ι), f a ^ p) ^ (1 / p) + (∑' (a : ι), g a ^ p) ^ (1 / p)
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: case inl
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : 0 ≤ c
⊢ ‖f‖ ≤ c * ‖g‖

Tactic:
lift c to ℝ≥0 using hc
    exact NNReal.coe_le_coe.mpr (nnnorm_le_mul_nnnorm_of_ae_le_mul h)

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
convert! this using 1 <;> [skip; congr 2] <;> [skip; skip; simp; skip; simp] <;>
    · refine Finset.sum_congr rfl fun i hi => ?_
      simp [H'.1 i hi, H'.2 i hi, -WithZero.coe_mul]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case pos
ι : 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 = 0) ∨ ∀ i ∈ s, w i = 0 ∨ f i = 0
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

Tactic:
have (i) (hi : i ∈ s) : w i * f i = 0 := by rcases H with H | H <;> simp [H i hi]

Goal state after:
case pos
ι : 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 = 0) ∨ ∀ i ∈ s, w i = 0 ∨ f i = 0
this : ∀ i ∈ s, w i * f i = 0
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case pos.inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
H' : (∑ i ∈ s, f i ^ p) ^ (1 / p) = ∞
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)

Tactic:
simp [H', -one_div]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case pos.inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
H' : (∑ i ∈ s, g i ^ p) ^ (1 / p) = ∞
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)

Tactic:
simp [H', -one_div]

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 => ?_

Goal state after:
case refine_1
𝕜 : 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
x : E
⊢ ‖((lsmul 𝕜 R) a) x‖ ≤ ‖a‖ * ‖x‖

case refine_2
𝕜 : 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
N : ℝ
x✝ : N ≥ 0
h : ∀ (x : E), ‖((lsmul 𝕜 R) a) x‖ ≤ N * ‖x‖
⊢ ‖a‖ ≤ N
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: case mp
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
ι : Type u_9
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
tfae_4_iff_5 : (∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖
tfae_5_iff_7 : (∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (Set.range fun x ↦ ‖f x‖)
tfae_6_iff_8 : (∃ C, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (Set.range fun x ↦ ‖f x‖)
tfae_8_iff_9 : BddAbove (Set.range fun x ↦ ‖f x‖) ↔ ⨆ i, ↑‖f i‖₊ < ⊤
⊢ (∃ p,
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑p ∧
        ∀ (k : ι), (normSeminorm 𝕜₂ F).comp ↑(f k) ≤ p) →
    ∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖

Tactic:
intro ⟨p, hp, hpf⟩
      rcases p.bound_of_continuous_normedSpace hp with ⟨C, -, hC⟩
      exact ⟨C, fun i x ↦ (hpf i x).trans (hC x)⟩

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
ι : Type u_9
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
tfae_4_iff_5 : (∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖
tfae_5_iff_7 : (∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (Set.range fun x ↦ ‖f x‖)
tfae_6_iff_8 : (∃ C, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (Set.range fun x ↦ ‖f x‖)
tfae_8_iff_9 : BddAbove (Set.range fun x ↦ ‖f x‖) ↔ ⨆ i, ↑‖f i‖₊ < ⊤
⊢ (∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) →
    ∃ p,
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑p ∧
        ∀ (k : ι), (normSeminorm 𝕜₂ F).comp ↑(f k) ≤ p

Tactic:
intro ⟨C, hC⟩

Goal state after:
case mpr
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
ι : Type u_9
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
tfae_4_iff_5 : (∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖
tfae_5_iff_7 : (∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (Set.range fun x ↦ ‖f x‖)
tfae_6_iff_8 : (∃ C, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (Set.range fun x ↦ ‖f x‖)
tfae_8_iff_9 : BddAbove (Set.range fun x ↦ ‖f x‖) ↔ ⨆ i, ↑‖f i‖₊ < ⊤
C : ℝ
hC : ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖
⊢ ∃ p,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑p ∧
      ∀ (k : ι), (normSeminorm 𝕜₂ F).comp ↑(f k) ≤ p
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 : IsTopCompl p q
hq : IsClosed[inst✝³] ↑q
⊢ T3Space ↥p

Tactic:
by
  have : IsClosed ({0} : Set p) := by
    rw [← (isQuotientMap_projectionOntoL h).isClosed_preimage]
    rwa [← ker_projectionOntoL h] at hq
  have : T1Space p := IsTopologicalAddGroup.t1Space _ this
  rw [RegularSpace.t3Space_iff_t0Space]
  infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : μ u ≠ ∞
⊢ (s ∩ t).Nonempty

Tactic:
rw [add_comm] at h

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real t + μ.real s
hu : μ u ≠ ∞
⊢ (s ∩ t).Nonempty
Module: Mathlib.Order.Filter.IndicatorFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : One β
l : Filter α
f : α → β
s : Set α
hf : f =ᶠ[l] 1
⊢ s.mulIndicator 1 =ᶠ[l] 1

Tactic:
mulIndicator_one'

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : One β
l : Filter α
f : α → β
s : Set α
hf : f =ᶠ[l] 1
⊢ 1 =ᶠ[l] 1
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ Integrable (fun x ↦ ‖f x‖ₑ ^ p.toReal) μ

Tactic:
rw [← memLp_one_iff_integrable]
  exact hf.enorm_rpow hp_ne_zero hp_ne_top

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

Goal state before:
pp: α : Type u_1
ε : Type u_5
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : PseudoMetrizableSpace ε
ι : Type u_8
m : MeasurableSpace α
f : α → ε
μ : ι → Measure α
s : Finset ι
⊢ Integrable f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)

Tactic:
induction s using Finset.induction_on <;> simp [*]

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) μ
⊢ Integrable f μ

Tactic:
refine h_int.mono' h_meas ?_
  filter_upwards [hf, hg] with a haf hag
  exact (Real.norm_of_nonneg haf).symm ▸ le_add_of_nonneg_right hag

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

Goal state before:
pp: case mp
α : 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 ∈ map e l ∧ IntegrableOn (f ∘ e) (e ⁻¹' s) μ
⊢ ∃ s ∈ l, IntegrableOn (f ∘ e) s μ

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 ⟨_, hs⟩

Goal state after:
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) μ
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : UniformSpace E
inst✝⁴ : T2Space E
inst✝³ : IsUniformAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
⊢ CompleteSpace E

Tactic:
set e := ContinuousLinearEquiv.ofFinrankEq (@finrank_fin_fun 𝕜 _ _ (finrank 𝕜 E)).symm
  have : IsUniformEmbedding e.toEquiv.symm := e.symm.isUniformEmbedding
  exact (completeSpace_congr this).1 inferInstance

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : CompleteSpace 𝕜
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : ContinuousSMul 𝕜 F
E : Type u_4
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
f : E →ₗ[𝕜] F
s : Submodule 𝕜 E
inst✝ : s.CoFG
h : IsClosed[inst✝⁶] ↑(Submodule.map f s)
t : Submodule 𝕜 E
s_compl_t : IsCompl s t
⊢ IsClosed[inst✝⁶] ↑f.range

Tactic:
have : FiniteDimensional 𝕜 t := .of_fg <| Submodule.CoFG.fg_of_isCompl s_compl_t inferInstance

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : CompleteSpace 𝕜
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : ContinuousSMul 𝕜 F
E : Type u_4
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
f : E →ₗ[𝕜] F
s : Submodule 𝕜 E
inst✝ : s.CoFG
h : IsClosed[inst✝⁶] ↑(Submodule.map f s)
t : Submodule 𝕜 E
s_compl_t : IsCompl s t
this : FiniteDimensional 𝕜 ↥t
⊢ IsClosed[inst✝⁶] ↑f.range
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: case inl
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace E
inst✝² : Countable ι
f : ι → X → E
hE : Nonempty E
inst✝¹ : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
inst✝ : ⊥.IsCountablyGenerated
⊢ StronglyMeasurable fun x ↦ ⊥.limUnder fun x_1 ↦ f x_1 x

pp: case inr
ι : 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
⊢ StronglyMeasurable fun x ↦ l.limUnder fun x_1 ↦ f x_1 x

Tactic:
· simpa [limUnder, Filter.map_bot] using stronglyMeasurable_const

Goal state after:
case inr
ι : 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
⊢ StronglyMeasurable fun x ↦ l.limUnder fun x_1 ↦ f x_1 x