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

Goal state before:
pp: case inr
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
repeat' rw [ENNReal.rpow_one] at h

Goal state after:
case inr
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
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 : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x ↦ 1
h_rw : ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ = ∫⁻ (a : α), (‖f a‖ₑ * g a) ^ p ∂μ
r : ℝ := p * q / (q - p)
hpqr : 1 / p = 1 / q + 1 / r
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r) =
    (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) * μ Set.univ ^ (1 / p - 1 / q)

Tactic:
by
      rw [hpqr]; simp [r, g]

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

Goal state before:
pp: case refine_3.some
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
i : ι
hi : some i ∈ insertNone s
⊢ 0 ≤ (some i).elim q p

Tactic:
refine hp i ?_

Goal state after:
case refine_3.some
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
i : ι
hi : some i ∈ insertNone s
⊢ i ∈ s
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 μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h :
  ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / q)
⊢ 1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))

Tactic:
have h_one_div_q : 1 / q = 1 - 1 / p := by
    nth_rw 2 [← hpq.inv_add_inv_eq_one]
    ring

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h :
  ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / q)
h_one_div_q : 1 / q = 1 - 1 / p
⊢ 1 ≤
    (∫⁻ (a : α), (f + 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: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp : 0 < p
hf : eLpNorm (↑↑f) p μ = 0 ∨ False
⊢ f = 0

Tactic:
or_false

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp : 0 < p
hf : eLpNorm (↑↑f) p μ = 0
⊢ f = 0
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

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

pp: case ha
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ≥0
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
this : eLpNorm (↑↑f) p μ ≤ c • eLpNorm (↑↑g) p μ
⊢ eLpNorm (↑↑f) p μ ≠ ∞

pp: case hb
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ≥0
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
this : eLpNorm (↑↑f) p μ ≤ c • eLpNorm (↑↑g) p μ
⊢ c • eLpNorm (↑↑g) p μ ≠ ∞

Tactic:
ENNReal.toNNReal_coe

Goal state after:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ≥0
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
this : (eLpNorm (↑↑f) p μ).toNNReal ≤ c * (eLpNorm (↑↑g) p μ).toNNReal
⊢ (eLpNorm (↑↑f) p μ).toNNReal ≤ c * (eLpNorm (↑↑g) p μ).toNNReal

case ha
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ≥0
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
this : eLpNorm (↑↑f) p μ ≤ c • eLpNorm (↑↑g) p μ
⊢ eLpNorm (↑↑f) p μ ≠ ∞

case hb
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ≥0
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
this : eLpNorm (↑↑f) p μ ≤ c • eLpNorm (↑↑g) p μ
⊢ c • eLpNorm (↑↑g) p μ ≠ ∞
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
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h : (∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_integral : ∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ < ∞
⊢ ∀ᵐ (x : α) ∂μ, ∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ < ∞

Tactic:
have rpow_ae_lt_top : ∀ᵐ x ∂μ, (∑' i, ‖f (i + 1) x - f i x‖ₑ) ^ p < ∞ := by
    refine ae_lt_top' (AEMeasurable.pow_const ?_ _) h_integral.ne
    exact AEMeasurable.tsum fun n => ((hf (n + 1)).sub (hf n)).enorm

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h : (∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_integral : ∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ < ∞
rpow_ae_lt_top : ∀ᵐ (x : α) ∂μ, (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) ^ p < ∞
⊢ ∀ᵐ (x : α) ∂μ, ∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ < ∞
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: 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 : g b₁ = g b₂
⊢ Sum.inr b₁ = Sum.inr b₂

Tactic:
g.injective f_eq

Goal state after:
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 : g b₁ = g b₂
⊢ Sum.inr b₂ = Sum.inr b₂
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
a✝ : Nontrivial R
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | IsUnit x}

Tactic:
Metric.isOpen_iff

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
a✝ : Nontrivial R
⊢ ∀ x ∈ {x | IsUnit x}, ∃ ε > 0, Metric.ball x ε ⊆ {x | IsUnit x}
Module: Mathlib.Analysis.Normed.Ring.Units

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

Tactic:
by
  simpa using inverse_add_norm_diff_nth_order x 1

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₁ : Type u_2
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
Fₗ : Type u_7
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
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ : E →SL[σ₁₂] F
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₁₃
a : F →ₛₗᵢ[σ₂₃] G
f : E →SL[σ₁₂] F
⊢ ‖{ toFun := fun f ↦ a.toContinuousLinearMap ∘SL f, map_add' := ⋯, map_smul' := ⋯ } f‖ = ‖f‖

Tactic:
by simp [a.norm_toContinuousLinearMap_comp]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
X : Type u_5
inst✝ : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
s : Set X
x : X
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
⊢ ContinuousWithinAt (fun x ↦ (f x).coprod (g x)) s x

Tactic:
simp only [← comp_fst_add_comp_snd]
  fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
X : Type u_5
inst✝ : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt (fun x ↦ (f x).coprod (g x)) x

Tactic:
simp only [← comp_fst_add_comp_snd]
  fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
X : Type u_5
inst✝ : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
s : Set X
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn (fun x ↦ (f x).coprod (g x)) s

Tactic:
simp only [← comp_fst_add_comp_snd]
  fun_prop

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

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

Tactic:
hU

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝⁸ : NormedField 𝕜
inst✝⁷ : (i : ι) → TopologicalSpace (E i)
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
S : Set (ContinuousMultilinearMap 𝕜 E F)
hS : IsVonNBounded 𝕜 S
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
U : Set F
hU : U ∈ 𝓝 0
⊢ Absorbs 𝕜 U (image2 (fun f x ↦ f x) S s)
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommGroup (E i)
inst✝⁸ : (i : ι) → Module 𝕜 (E i)
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (E₁ i)
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝ : (i : ι) → Module 𝕜 (E₁ i)
f : (i : ι) → E i →L[𝕜] E₁ i
aux : ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F :=
  { toFun := fun g ↦ g.compContinuousLinearMap f, map_add' := ⋯, map_smul' := ⋯ }
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] aux.toFun

Tactic:
apply continuous_of_tendsto_nhds_zero aux

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommGroup (E i)
inst✝⁸ : (i : ι) → Module 𝕜 (E i)
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (E₁ i)
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝ : (i : ι) → Module 𝕜 (E₁ i)
f : (i : ι) → E i →L[𝕜] E₁ i
aux : ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F := ⋯
⊢ Filter.Tendsto (⇑aux) (𝓝 0) (𝓝 0)
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommGroup (E i)
inst✝⁸ : (i : ι) → Module 𝕜 (E i)
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (E₁ i)
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝ : (i : ι) → Module 𝕜 (E₁ i)
f : (i : ι) → E i →L[𝕜] E₁ i
aux : ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F :=
  { toFun := fun g ↦ g.compContinuousLinearMap f, map_add' := ⋯, map_smul' := ⋯ }
⊢ ∀ (ib : Set ((i : ι) → E i) × Set F),
    IsVonNBounded 𝕜 ib.1 ∧ ib.2 ∈ 𝓝 0 →
      ∃ ia, (IsVonNBounded 𝕜 ia.1 ∧ ia.2 ∈ 𝓝 0) ∧ ∀ x ∈ {f | MapsTo (⇑f) ia.1 ia.2}, aux x ∈ {f | MapsTo (⇑f) ib.1 ib.2}

Tactic:
rintro ⟨U, V⟩ ⟨hU, hV⟩

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommGroup (E i)
inst✝⁸ : (i : ι) → Module 𝕜 (E i)
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (E₁ i)
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝ : (i : ι) → Module 𝕜 (E₁ i)
f : (i : ι) → E i →L[𝕜] E₁ i
aux : ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F :=
  { toFun := fun g ↦ g.compContinuousLinearMap f, map_add' := ⋯, map_smul' := ⋯ }
U : Set ((i : ι) → E i)
V : Set F
hU : IsVonNBounded 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
⊢ ∃ ia,
    (IsVonNBounded 𝕜 ia.1 ∧ ia.2 ∈ 𝓝 0) ∧ ∀ x ∈ {f | MapsTo (⇑f) ia.1 ia.2}, aux x ∈ {f | MapsTo ⇑f (U, V).1 (U, V).2}
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
aux₁ : ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := g.compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯ }
⊢ ∀ (ib : Set ((i : ι) → E i) × Set G),
    IsVonNBounded 𝕜 ib.1 ∧ ib.2 ∈ 𝓝 0 →
      ∃ ia,
        (IsVonNBounded 𝕜 ia.1 ∧ ia.2 ∈ 𝓝 0) ∧ ∀ x ∈ {f | MapsTo (⇑f) ia.1 ia.2}, aux₁ x ∈ {f | MapsTo (⇑f) ib.1 ib.2}

Tactic:
rintro ⟨U, V⟩ ⟨hU, hV⟩

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
aux₁ : ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := g.compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯ }
U : Set ((i : ι) → E i)
V : Set G
hU : IsVonNBounded 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
⊢ ∃ ia,
    (IsVonNBounded 𝕜 ia.1 ∧ ia.2 ∈ 𝓝 0) ∧ ∀ x ∈ {f | MapsTo (⇑f) ia.1 ia.2}, aux₁ x ∈ {f | MapsTo ⇑f (U, V).1 (U, V).2}
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
aux : (F →L[𝕜] G) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := fun g ↦ { toFun := g.compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
    map_add' := ⋯, map_smul' := ⋯ }
⊢ Continuous[topologicalSpace, topologicalSpace] aux.toFun

Tactic:
apply continuous_of_tendsto_nhds_zero aux

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
aux : (F →L[𝕜] G) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G := ⋯
⊢ Filter.Tendsto (⇑aux) (𝓝 0) (𝓝 0)
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
h : IsCompl p q
⊢ Continuous[inst✝², inst✝²] ⇑(p.projection q h) ↔
    Continuous[inst✝², instTopologicalSpaceSubtype] ⇑(p.projectionOnto q h)

Tactic:
IsInducing.subtypeVal.continuous_iff

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
h : IsCompl p q
⊢ Continuous[inst✝², inst✝²] ⇑(p.projection q h) ↔ Continuous[inst✝², inst✝²] (Subtype.val ∘ ⇑(p.projectionOnto q h))
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
C : ε'
hC : ‖C‖ₑ ≠ ∞
⊢ IntegrableOn (fun x ↦ C) s μ ↔ ‖C‖ₑ = 0 ∨ μ s < ∞

Tactic:
rw [IntegrableOn, integrable_const_iff_enorm hC, isFiniteMeasure_restrict, lt_top_iff_ne_top]

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

Goal state before:
pp: case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : ¬finrank 𝕜 ↥l.range = 0
this : finrank 𝕜 ↥l.range = 1
hi : Function.Injective ⇑(l.ker.liftQ l ⋯)
hs : Function.Surjective ⇑(l.ker.liftQ l ⋯)
⊢ Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑l

Tactic:
let φ : (E ⧸ LinearMap.ker l) ≃ₗ[𝕜] 𝕜 :=
      LinearEquiv.ofBijective ((LinearMap.ker l).liftQ l (le_refl _)) ⟨hi, hs⟩

Goal state after:
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : ¬finrank 𝕜 ↥l.range = 0
this : finrank 𝕜 ↥l.range = 1
hi : Function.Injective ⇑(l.ker.liftQ l ⋯)
hs : Function.Surjective ⇑(l.ker.liftQ l ⋯)
φ : (E ⧸ l.ker) ≃ₗ[𝕜] 𝕜 := LinearEquiv.ofBijective (l.ker.liftQ l ⋯) ⋯
⊢ Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑l
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ IsSeparable (f '' s)

pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ f '' s

Tactic:
· exact (hs.image_of_continuousOn hf).isSeparable

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ f '' s
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : CompactSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
μ : Measure α
f : α → β
hf : Continuous[inst✝⁴, inst✝¹] f
⊢ AEStronglyMeasurable f μ

Tactic:
by
  simpa using hf.continuousOn.aestronglyMeasurable_of_isCompact isCompact_univ .univ

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
b : E
x✝ : b ∈ f.range
⊢ μ.real (⇑f ⁻¹' {b}) * (ENNReal.toReal ∘ g) b = (g b * μ (⇑f ⁻¹' {b})).toReal

Tactic:
toReal_mul,

Goal state after:
α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
b : E
x✝ : b ∈ f.range
⊢ μ.real (⇑f ⁻¹' {b}) * (ENNReal.toReal ∘ g) b = (g b).toReal * (μ (⇑f ⁻¹' {b})).toReal