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

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

Tactic:
top_rpow_of_pos hp_pos

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

Goal state before:
pp: case pos
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : p = ∞
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ

pp: case neg
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ

Tactic:
· simp [hp_top, eLpNormEssSup_add_le]

Goal state after:
case neg
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case refine_3
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
n : ℝ := ∑ i ∈ s, w i
hw' : 0 < n
this : (∑ i ∈ s, w i / n / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ (w i / n)
⊢ n / ∑ i ∈ s, w i / z i ≤ (∏ i ∈ s, z i ^ w i) ^ n⁻¹

Tactic:
div_eq_mul_inv,

Goal state after:
case refine_3
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
n : ℝ := ∑ i ∈ s, w i
hw' : 0 < n
this : (∑ i ∈ s, w i / n / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ (w i / n)
⊢ n * (∑ i ∈ s, w i / z i)⁻¹ ≤ (∏ i ∈ s, z i ^ w i) ^ n⁻¹
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
⊢ ∫⁻ (a : α), 2 ^ (p - 1) * f a ^ p + 2 ^ (p - 1) * g a ^ p ∂μ < ∞

Tactic:
rw [lintegral_add_left', lintegral_const_mul'' _ (hf.pow_const p),
        lintegral_const_mul' _ _ (by finiteness), ENNReal.add_lt_top]
      · constructor <;> finiteness
      · fun_prop

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case refine_3
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
this : (∑ i ∈ s, (w i / ∑ i ∈ s, w i) / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ (w i / ∑ i ∈ s, w i)
⊢ (∑ i ∈ s, w i) / ∑ i ∈ s, w i / z i ≤ (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹

pp: case refine_1
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
⊢ ∀ i ∈ s, 0 < w i / ∑ i ∈ s, w i

pp: case refine_2
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
⊢ ∑ i ∈ s, w i / ∑ i ∈ s, w i = 1

Tactic:
· set n := ∑ i ∈ s, w i
    nth_rw 1 [div_eq_mul_inv, (show n = (n⁻¹)⁻¹ by simp), ← mul_inv, Finset.mul_sum _ _ n⁻¹]
    simp_rw [inv_mul_eq_div n ((w _) / (z _)), div_right_comm _ _ n]
    convert! this
    rw [← Real.finsetProd_rpow s _ (fun i hi ↦ by positivity [hz i hi])]
    refine Finset.prod_congr rfl (fun i hi => ?_)
    rw [← Real.rpow_mul (le_of_lt <| hz i hi) (w _) n⁻¹, div_eq_mul_inv (w _) n]

Goal state after:
case refine_1
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
⊢ ∀ i ∈ s, 0 < w i / ∑ i ∈ s, w i

case refine_2
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
⊢ ∑ i ∈ s, w i / ∑ i ∈ s, w i = 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
ι : Type u_4
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
⊢ Tendsto f fi (𝓝 f_lim) ↔ Tendsto (fun n ↦ eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (𝓝 0)

Tactic:
rw [tendsto_iff_dist_tendsto_zero]

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
⊢ Tendsto (fun b ↦ dist (f b) f_lim) fi (𝓝 0) ↔ Tendsto (fun n ↦ eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (𝓝 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∞
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
⊢ {x | ε ≤ edist (f' i x) (g' x)} =ᵐ[μ] {x | ε ≤ edist (f i x) (g x)}

Tactic:
filter_upwards [h_ae_eq, h_right] with x hxf hxg

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 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ {x | ε ≤ edist (f' i x) (g' x)} x = {x | ε ≤ edist (f i x) (g x)} x
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm f (p / q * q) μ ≠ ∞

Tactic:
div_eq_mul_inv,

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm f (p * q⁻¹ * q) μ ≠ ∞
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm f (p / q * q) μ ≠ ∞

Tactic:
div_eq_mul_inv,

Goal state after:
case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm f (p * q⁻¹ * q) μ ≠ ∞
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: case e'_7
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
⊢ p = p / q / q⁻¹

Tactic:
div_eq_mul_inv,

Goal state after:
case e'_7
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
⊢ p = p / q * q⁻¹⁻¹
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: case e'_7
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
⊢ p = p / q * q

Tactic:
div_eq_mul_inv,

Goal state after:
case e'_7
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
⊢ p = p * q⁻¹ * q
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: case e'_7
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ ^ q.toReal) (p / q) μ
⊢ p = p / q / q⁻¹

Tactic:
div_eq_mul_inv,

Goal state after:
case e'_7
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ ^ q.toReal) (p / q) μ
⊢ p = p / q * q⁻¹⁻¹
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: case e'_7
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ ^ q.toReal) (p / q) μ
⊢ p = p / q * q

Tactic:
div_eq_mul_inv,

Goal state after:
case e'_7
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ ^ q.toReal) (p / q) μ
⊢ p = p * q⁻¹ * q
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ 1 = p / p

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
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: α : 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

Tactic:
div_eq_mul_inv,

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: α : 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✝
g✝ : E → F✝
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜'
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' F✝
σ : 𝕜 →+* 𝕜'
inst✝⁴ : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
g h : G
⊢ compLpₗ p μ (B (g + h)) = compLpₗ p μ (B g) + compLpₗ p μ (B h)

Tactic:
by
    ext f
    filter_upwards [(B (g + h)).coeFn_compLp f, (B g).coeFn_compLp f, (B h).coeFn_compLp f,
      Lp.coeFn_add ((B g).compLp f) ((B h).compLp f)] with x hx hg hh hadd
    simp only [compLpₗ_apply, LinearMap.add_apply, hx, hadd]
    simp only [map_add, add_apply, Pi.add_apply, hg, hh]

Goal state after:
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 := ⋯ }
⊢ Absorbs 𝕜 V (⇑f '' s)

Tactic:
obtain ⟨I, t, ht₀, hft⟩ :
        ∃ (I : Finset ι) (t : ∀ i, Set (E i)), (∀ i, t i ∈ 𝓝 0) ∧ Set.pi I t ⊆ f ⁻¹' V := by
      have hfV : f ⁻¹' V ∈ 𝓝 0 := (map_continuous f).tendsto' _ _ f.map_zero hV
      rwa [nhds_pi, Filter.mem_pi, exists_finite_iff_finset] at hfV

Goal state after:
ι : 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
⊢ Absorbs 𝕜 V (⇑f '' s)
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: case inl
ι : 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) • x i ∈ t i

Tactic:
refine hc _ _ ?_ _ hx

Goal state after:
case inl
ι : 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‖ ≤ ‖c i‖
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: case hbc
ι : 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 𝕜 := ⋯
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 : ι
hi : i ∈ ↑I
⊢ ‖∏ i ∈ I, c i‖ / ‖∏ i ∈ I, c i‖ ≤ 1

Tactic:
apply div_self_le_one

Goal state after:
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
i₀ : ι
y : (i : ι) → E i := I.piecewise (fun i ↦ c i • x i) x
⊢ (a / ∏ i ∈ I, c i) • (∏ i ∈ I, c i) • f x = a • f x

Tactic:
div_eq_mul_inv,

Goal state after:
ι : 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
i₀ : ι
y : (i : ι) → E i := I.piecewise (fun i ↦ c i • x i) x
⊢ (a * (∏ i ∈ I, c i)⁻¹) • (∏ i ∈ I, c i) • f x = a • f x
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✝⁸ : UniformSpace F✝
inst✝⁷ : IsUniformAddGroup F✝
inst✝⁶ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
hF : T2Space F
H :
  ∀ {m : (i : ι) → E i},
    Continuous[topologicalSpace ((i : ι) → E i) F {s | IsVonNBounded 𝕜 s}, inst✝³.toTopologicalSpace] fun f ↦
      (toFun {s | IsVonNBounded 𝕜 s}) f m
⊢ IsComplete (range toUniformOnFun)

Tactic:
range_toUniformOnFun

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✝⁸ : UniformSpace F✝
inst✝⁷ : IsUniformAddGroup F✝
inst✝⁶ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
hF : T2Space F
H :
  ∀ {m : (i : ι) → E i},
    Continuous[topologicalSpace ((i : ι) → E i) F {s | IsVonNBounded 𝕜 s}, inst✝³.toTopologicalSpace] fun f ↦
      (toFun {s | IsVonNBounded 𝕜 s}) f m
⊢ IsComplete
    {f |
      Continuous[Pi.topologicalSpace, inst✝³.toTopologicalSpace] ((toFun {s | IsVonNBounded 𝕜 s}) f) ∧
        (∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
            (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (x + y)) =
              (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x) + (toFun {s | IsVonNBounded 𝕜 s}) f (update m i y)) ∧
          ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
            (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (c • x)) =
              c • (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x)}
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
this : IsIdempotentElem 0
⊢ IsTopCompl ⊥ ⊤

Tactic:
simpa using this.isTopCompl

Goal state after:
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
this : IsIdempotentElem (ContinuousLinearMap.id R M)
⊢ IsTopCompl ⊤ ⊥

Tactic:
simpa using this.isTopCompl

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
this : μ (s ∪ t) ≠ ∞
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t

Tactic:
rw [← measureReal_inter_add_sdiff₀ ht this, Set.union_inter_cancel_right, union_sdiff_right,
    ← measureReal_inter_add_sdiff₀ ht h₁]

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
this : μ (s ∪ t) ≠ ∞
⊢ μ.real t + μ.real (s \ t) + μ.real (s ∩ t) = μ.real (s ∩ t) + μ.real (s \ t) + μ.real t
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 : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), μ (t b) ≠ ∞
hp : p ≠ ∞
h : Tendsto (fun b ↦ μ (t b ∆ s)) l (𝓝 0)
⊢ Tendsto (fun b ↦ indicatorConstLp p ⋯ ⋯ c) l (𝓝 (indicatorConstLp p hs hμs c))

Tactic:
rw [tendsto_iff_dist_tendsto_zero]

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 : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), μ (t b) ≠ ∞
hp : p ≠ ∞
h : Tendsto (fun b ↦ μ (t b ∆ s)) l (𝓝 0)
⊢ Tendsto (fun b ↦ dist (indicatorConstLp p ⋯ ⋯ c) (indicatorConstLp p hs hμs c)) l (𝓝 0)
Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp f p μ

Tactic:
rw [← Set.indicator_add_eq_left h]; exact hfg.indicator (measurableSet_support hf.measurable)

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:
by
  classical
  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 α
ε' : Type u_8
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddCommMonoid ε'
inst✝ : ContinuousAdd ε'
ι : Type u_9
s : Finset ι
f : ι → α → ε'
hf : ∀ i ∈ s, Integrable (f i) μ
⊢ Integrable (fun a ↦ ∑ i ∈ s, f i a) μ

Tactic:
by
  simpa only [← Finset.sum_apply] using integrable_finsetSum' s hf

Goal state after: