mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ q) (B ^ q)
H₁ : Summable fun i ↦ f i * g i
H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
⊢ B = (∑' (i : ι), g i ^ q) ^ (1 / q)

Tactic:
hg.tsum_eq,

Goal state after:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ q) (B ^ q)
H₁ : Summable fun i ↦ f i * g i
H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
⊢ B = (B ^ q) ^ (1 / q)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i ↦ (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
⊢ B = (∑' (i : ι), g i ^ p) ^ (1 / p)

Tactic:
hg.tsum_eq,

Goal state after:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i ↦ (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
⊢ B = (B ^ p) ^ (1 / p)
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
f : ι → α → E
l : Filter ι
g : α → E
h : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
a : α
⊢ ε ≤ dist (f i a) (g a) ↔ ENNReal.ofReal ε ≤ ENNReal.ofReal (dist (f i a) (g a))

Tactic:
ENNReal.ofReal_le_ofReal_iff (by positivity)

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
a : α
⊢ ε ≤ dist (f i a) (g a) ↔ ε ≤ dist (f i a) (g a)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ≥0
⊢ ∑ i ∈ s, (fun i ↦ ↑(w i)) i * (fun i ↦ ↑(f i)) i ≤
    (∑ i ∈ s, (fun i ↦ ↑(w i)) i) ^ (1 - p⁻¹) * (∑ i ∈ s, (fun i ↦ ↑(w i)) i * (fun i ↦ ↑(f i)) i ^ p) ^ p⁻¹

Tactic:
beta_reduce at *

Goal state after:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ≥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: ι : Type u
p q r : ℝ
hpqr : p.HolderTriple q r
f : ι → ℝ≥0
hf_sum : Summable fun i ↦ (fun i ↦ ↑(f i)) i ^ p
g : ι → ℝ≥0
hg_sum : Summable fun i ↦ (fun i ↦ ↑(g i)) i ^ q
⊢ (Summable fun i ↦ ((fun i ↦ ↑(f i)) i * (fun i ↦ ↑(g i)) i) ^ r) ∧
    ∑' (i : ι), ((fun i ↦ ↑(f i)) i * (fun i ↦ ↑(g i)) i) ^ r ≤
      (∑' (i : ι), (fun i ↦ ↑(f i)) i ^ p) ^ (r / p) * (∑' (i : ι), (fun i ↦ ↑(g i)) i ^ q) ^ (r / q)

Tactic:
beta_reduce at *

Goal state after:
ι : Type u
p q r : ℝ
hpqr : p.HolderTriple q r
f : ι → ℝ≥0
hf_sum : Summable fun i ↦ ↑(f i) ^ p
g : ι → ℝ≥0
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)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
f g : ι → ℝ≥0
A : ℝ≥0
hf_sum : HasSum (fun i ↦ (fun i ↦ ↑(f i)) i ^ p) (↑A ^ p)
B : ℝ≥0
hg_sum : HasSum (fun i ↦ (fun i ↦ ↑(g i)) i ^ q) (↑B ^ q)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A * ↑B ∧ HasSum (fun i ↦ (fun i ↦ ↑(f i)) i * (fun i ↦ ↑(g i)) i) C

Tactic:
beta_reduce at *

Goal state after:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
f g : ι → ℝ≥0
A : ℝ≥0
hf_sum : HasSum (fun i ↦ ↑(f i) ^ p) (↑A ^ p)
B : ℝ≥0
hg_sum : HasSum (fun i ↦ ↑(g i) ^ q) (↑B ^ q)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A * ↑B ∧ HasSum (fun i ↦ ↑(f i) * ↑(g i)) C
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
beta_reduce at *

Goal state after:
ι : 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)
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns → ∃ ns', StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun i ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
ε : ℝ≥0∞
hε : 0 < ε
h2 : ¬Tendsto (fun i ↦ (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) atTop (𝓝 0)
⊢ ∃ δ ns, 0 < δ ∧ StrictMono ns ∧ ∀ (n : ℕ), δ ≤ (μ {x | ε ≤ edist (f (ns n) x) (g x)}).toNNReal

Tactic:
obtain ⟨s, hs, h4⟩ := not_tendsto_iff_exists_frequently_notMem.1 h2
    obtain ⟨δ, hδ, h5⟩ := NNReal.nhds_zero_basis.mem_iff.1 hs
    obtain ⟨ns, hns, h6⟩ := extraction_of_frequently_atTop h4
    exact ⟨δ, ns, hδ, hns, fun n ↦ Set.notMem_Iio.1 (Set.notMem_subset h5 (h6 n))⟩

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✝² : EMetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
ns : ℕ → ι
h1 : Tendsto ns atTop u
h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ns i) x) atTop (𝓝 (g x))
ns' : ℕ → ℕ
h2 : Tendsto ns' atTop atTop
h2' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ (f ∘ ns) (ns' i) x) atTop (𝓝 (h x))
ω : α
hg1 : Tendsto (fun i ↦ f (ns i) ω) atTop (𝓝 (g ω))
hh1 : Tendsto (fun i ↦ (f ∘ ns) (ns' i) ω) atTop (𝓝 (h ω))
⊢ g ω = h ω

Tactic:
exact tendsto_nhds_unique (hg1.comp h2) hh1

Goal state after:
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
⊢ Function.Injective fun x ↦
    match x with
    | Sum.inl a => f a
    | Sum.inr b => g b

Tactic:
rintro (a₁ | b₁) (a₂ | b₂) f_eq

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
a₁ a₂ : α
f_eq :
  (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inl a₁) =
    (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inl a₂)
⊢ Sum.inl a₁ = Sum.inl a₂

case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
a₁ : α
b₂ : β
f_eq :
  (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inl a₁) =
    (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inr b₂)
⊢ Sum.inl a₁ = Sum.inr b₂

case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
b₁ : β
a₂ : α
f_eq :
  (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inr b₁) =
    (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inl a₂)
⊢ Sum.inr b₁ = Sum.inl a₂

case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
b₁ b₂ : β
f_eq :
  (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inr b₁) =
    (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inr b₂)
⊢ Sum.inr b₁ = Sum.inr b₂
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ μ {x | ε ≤ edist (f n x) (g x)} ≤ 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal

Tactic:
rw [one_div, ← ENNReal.inv_mul_le_iff, inv_inv]

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ ε ^ p.toReal * μ {x | ε ≤ edist (f n x) (g x)} ≤ eLpNorm (f n - g) p μ ^ p.toReal

case h1
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ (ε ^ p.toReal)⁻¹ ≠ 0

case h2
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ (ε ^ p.toReal)⁻¹ ≠ ∞
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∞
hε : ε > 0
⊢ ∃ N, B N ≤ ε

Tactic:
suffices h_tendsto_zero : ∃ N : ℕ, ∀ n : ℕ, N ≤ n → B n ≤ ε from
      ⟨h_tendsto_zero.choose, h_tendsto_zero.choose_spec _ le_rfl⟩

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 ≤ n → B n ≤ ε
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁷, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
y : (i : ι) → E i := I.piecewise (fun i ↦ c i • x i) x
i : ι
hi : i ∈ ↑I
⊢ ‖(a / ∏ i ∈ I, c i) * c i‖ ≤ ‖∏ i ∈ I, c i‖ / ‖∏ i ∈ I, c i‖ * ‖c i‖

Tactic:
by
              rw [norm_mul, norm_div]; gcongr; exact ha.out.le

Goal state after:
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 : Seminorm 𝕜 E
hp : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑p
hpf : ∀ (k : ι), (normSeminorm 𝕜₂ F).comp ↑(f k) ≤ p
⊢ ∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖

Tactic:
rcases p.bound_of_continuous_normedSpace hp with ⟨C, -, hC⟩

Goal state after:
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 : Seminorm 𝕜 E
hp : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑p
hpf : ∀ (k : ι), (normSeminorm 𝕜₂ F).comp ↑(f k) ≤ p
C : ℝ
hC : ∀ (x : E), p x ≤ C * ‖x‖
⊢ ∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖
Module: Mathlib.Topology.Algebra.Module.Determinant

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : CommRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousMul 𝕜
v : 𝕜
⊢ (toSpanSingleton 𝕜 v).det = v

Tactic:
rw [← smulRight_id, det_smulRight]; simp

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c c' : E
⊢ MemLp.toLp ((s.indicator fun x ↦ c) + s.indicator fun x ↦ c') ⋯ = MemLp.toLp (s.indicator fun x ↦ c + c') ⋯

Tactic:
indicator_add

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c c' : E
⊢ MemLp.toLp ((s.indicator fun x ↦ c) + s.indicator fun x ↦ c') ⋯ =
    MemLp.toLp (fun a ↦ s.indicator (fun x ↦ c) a + s.indicator (fun x ↦ c') a) ⋯
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
c : ε
hc : ‖c‖ₑ ≠ ∞
⊢ Integrable (fun x ↦ c) μ ↔ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ

Tactic:
have : AEStronglyMeasurable (fun _ : α => c) μ := aestronglyMeasurable_const

Goal state after:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
c : ε
hc : ‖c‖ₑ ≠ ∞
this : AEStronglyMeasurable (fun x ↦ c) μ
⊢ Integrable (fun x ↦ c) μ ↔ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst✝²] s
hs₂ : s.Nonempty
hs₃ : ∀ x ∈ s, l x ≠ 0
⊢ Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑l

Tactic:
by
  refine l.continuous_of_isClosed_ker (l.isClosed_or_dense_ker.resolve_right fun hl => ?_)
  rcases hs₂ with ⟨x, hx⟩
  have : x ∈ interior (LinearMap.ker l : Set E)ᶜ := by
    rw [mem_interior_iff_mem_nhds]
    exact mem_of_superset (hs₁.mem_nhds hx) hs₃
  rwa [hl.interior_compl] at this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
⊢ IntegrableAtFilter f (map e l) μ ↔ IntegrableAtFilter (f ∘ e) l (Measure.comap e μ)

Tactic:
simp_rw [← he.integrableAtFilter_map_iff, IntegrableAtFilter, he.map_comap]

Goal state after:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
⊢ (∃ s ∈ map e l, IntegrableOn f s μ) ↔ ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))
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 ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
I :
  ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ ≤
    C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
⊢ ‖f m₁ - f ((insert i s).piecewise m₂ m₁)‖ ≤
    ‖f m₁ - f (s.piecewise m₂ m₁)‖ + ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖

Tactic:
by
          rw [← dist_eq_norm, ← dist_eq_norm, ← dist_eq_norm]
          exact dist_triangle _ _ _

Goal state after:
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 : MultilinearMap 𝕜 E G
C : ℝ
D : ℝ := max C 1
D_pos : 0 ≤ D
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ D * ∏ i, ‖m i‖
m m' : (i : ι) → E i
h' : dist m' m < 1
this : max ‖m'‖ ‖m‖ ≤ ‖m‖ + 1
⊢ ‖f m' - f m‖ ≤ D * ↑(Fintype.card ι) * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖

Tactic:
calc
    ‖f m' - f m‖ ≤ D * Fintype.card ι * max ‖m'‖ ‖m‖ ^ (Fintype.card ι - 1) * ‖m' - m‖ :=
      f.norm_image_sub_le_of_bound D_pos H m' m
    _ ≤ D * Fintype.card ι * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖ := by gcongr

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

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
Eᵤ : Type u_6
inst✝⁵ : AddCommGroup Eᵤ
inst✝⁴ : Module 𝕜 Eᵤ
inst✝³ : UniformSpace Eᵤ
inst✝² : T2Space Eᵤ
inst✝¹ : IsUniformAddGroup Eᵤ
inst✝ : ContinuousSMul 𝕜 Eᵤ
x : Eᵤ
U : Set Eᵤ
hU_tb : TotallyBounded U
hU_nhds : -x +ᵥ U ∈ 𝓝 0
this : -x +ᵥ U = (fun x_1 ↦ x_1 - x) '' U
⊢ TotallyBounded (-x +ᵥ U)

Tactic:
exact this ▸ hU_tb.image (uniformContinuous_id.sub uniformContinuous_const)

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

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹² : Fintype ι'
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✝⁴ : 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‖
m : (i : ι) → E i
⊢ ‖{ toFun := fun m ↦ (f m).mkContinuous (C * ∏ i, ‖m i‖) ⋯, map_update_add' := ⋯, map_update_smul' := ⋯ } m‖ ≤
    max C 0 * ∏ i, ‖m i‖

Tactic:
simp only [coe_mk]
      refine ((f m).mkContinuous_norm_le' _).trans_eq ?_
      rw [max_mul_of_nonneg, zero_mul]
      positivity

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

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
G' : Type wG'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
g : G →ₗᵢ[𝕜] G'
f : ContinuousMultilinearMap 𝕜 E G
⊢ ‖g.toContinuousLinearMap.compContinuousMultilinearMap f‖ = ‖f‖

Tactic:
by
  simp only [ContinuousLinearMap.compContinuousMultilinearMap_coe,
    LinearIsometry.coe_toContinuousLinearMap, LinearIsometry.norm_map,
    ContinuousMultilinearMap.norm_def, Function.comp_apply]

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
inst✝⁶ : OpensMeasurableSpace X
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : T2Space X
𝕜 : Type u_9
inst✝³ : NormedRing 𝕜
inst✝² : SecondCountableTopologyEither X E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : X → 𝕜
g : X → E
s : Set X
hs : IsLocallyClosed s
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
⊢ LocallyIntegrableOn (fun x ↦ f x • g x) s μ

Tactic:
rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢
  exact fun k hk_sub hk_c => (hf k hk_sub hk_c).smul_continuousOn (hg.mono hk_sub) hk_c

Goal state after: