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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
h_eq : ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)
⊢ ∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k

Tactic:
by_contra!

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
h_eq : ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)
this : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k
⊢ False
Module: Mathlib.Analysis.Convex.Jensen

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, w j ≠ 0 → p j = ∑ i ∈ t, w i • p i

Tactic:
rw [← sum_filter_of_ne hw, ← sum_filter_of_ne hw', hf.map_sum_eq_iff]

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0
⊢ (∀ j ∈ {x ∈ t | w x ≠ 0}, p j = ∑ i ∈ t with w i ≠ 0, w i • p i) ↔
    ∀ j ∈ t, w j ≠ 0 → p j = ∑ x ∈ t with w x ≠ 0, w x • p x

case h₀
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0
⊢ ∀ i ∈ {x ∈ t | w x ≠ 0}, 0 < w i

case h₁
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0
⊢ ∑ i ∈ t with w i ≠ 0, w i = 1

case hmem
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0
⊢ ∀ i ∈ {x ∈ t | w x ≠ 0}, p i ∈ s
Module: Mathlib.Analysis.Convex.Jensen

Goal state before:
pp: 𝕜 : Type u_1
β : Type u_4
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set 𝕜
f : 𝕜 → β
x y z : 𝕜
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : z ∈ Set.Icc x y
⊢ f z ≤ max (f x) (f y)

Tactic:
rw [← segment_eq_Icc (hz.1.trans hz.2)] at hz; exact hf.le_max_of_mem_segment hx hy hz

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case mp
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h : Absorbs 𝕜 ((I.sup p).ball 0 1) s
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Tactic:
rcases h.exists_pos with ⟨r, hr, h⟩

Goal state after:
case mp
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h✝ : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
h : ∀ (c : 𝕜), r ≤ ‖c‖ → s ⊆ c • (I.sup p).ball 0 1
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case mpr
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
s' : Set E
hs'✝ : s' ∈ p.basisSets
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = (I.sup p).ball 0 r
r' : ℝ
left✝ : r' > 0
h' : ∀ x ∈ s, (I.sup p) x < r'
⊢ Absorbs 𝕜 ((I.sup p).ball 0 r) s

Tactic:
simp_rw [← (I.sup p).mem_ball_zero] at h'

Goal state after:
case mpr
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
s' : Set E
hs'✝ : s' ∈ p.basisSets
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = (I.sup p).ball 0 r
r' : ℝ
left✝ : r' > 0
h' : ∀ x ∈ s, x ∈ (I.sup p).ball 0 r'
⊢ Absorbs 𝕜 ((I.sup p).ball 0 r) s
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : FunLike 𝓕 E F
inst✝ : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑f
x : E
hx : ‖x‖ = 0
⊢ ‖f x‖ = 0

Tactic:
← mem_closure_zero_iff_norm,

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : FunLike 𝓕 E F
inst✝ : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑f
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {0}
⊢ f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {0}
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x y : E
⊢ ‖f (x - y)‖ ≤ ‖f‖ * ‖x - y‖

Tactic:
f.le_opNorm

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
Gₗ : Type u_9
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup Fₗ
inst✝⁴ : SeminormedAddCommGroup Gₗ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 Fₗ
inst✝ : NormedSpace 𝕜 Gₗ
f : E →L[𝕜] Fₗ →L[𝕜] Gₗ
x x' : E
y y' : Fₗ
⊢ (f (x + x')) (y + y') = (f x) y + (f.deriv₂ (x, y)) (x', y') + (f x') y'

Tactic:
simp only [map_add, add_apply, coe_deriv₂, add_assoc]
  abel

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
inst✝ : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : QuasiMeasurePreserving f μ ν
f' : α → β
hf' : Measurable f'
h : f =ᵐ[μ] f'
⊢ ↑(g.compQuasiMeasurePreserving f hf) =ᵐ[μ] ↑(g.compQuasiMeasurePreserving f' ⋯)

Tactic:
coeFn_compQuasiMeasurePreserving,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
inst✝ : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : QuasiMeasurePreserving f μ ν
f' : α → β
hf' : Measurable f'
h : f =ᵐ[μ] f'
⊢ ↑g ∘ f =ᵐ[μ] ↑(g.compQuasiMeasurePreserving f' ⋯)
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
inst✝ : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : QuasiMeasurePreserving f μ ν
f' : α → β
hf' : Measurable f'
h : f =ᵐ[μ] f'
⊢ ↑g ∘ f =ᵐ[μ] ↑(g.compQuasiMeasurePreserving f' ⋯)

Tactic:
coeFn_compQuasiMeasurePreserving,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
inst✝ : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : QuasiMeasurePreserving f μ ν
f' : α → β
hf' : Measurable f'
h : f =ᵐ[μ] f'
⊢ ↑g ∘ f =ᵐ[μ] ↑g ∘ f'
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_4
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace δ
inst✝ : MeasurableSpace β
ν : Measure β
γ : Type u_5
mγ : MeasurableSpace γ
ξ : Measure γ
g : γ →ₘ[ξ] δ
f : β → γ
hf : QuasiMeasurePreserving f ν ξ
f' : α → β
hf' : QuasiMeasurePreserving f' μ ν
⊢ ↑(g.compQuasiMeasurePreserving (f ∘ f') ⋯) =ᵐ[μ]
    ↑((g.compQuasiMeasurePreserving f hf).compQuasiMeasurePreserving f' hf')

Tactic:
coeFn_compQuasiMeasurePreserving,

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_4
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace δ
inst✝ : MeasurableSpace β
ν : Measure β
γ : Type u_5
mγ : MeasurableSpace γ
ξ : Measure γ
g : γ →ₘ[ξ] δ
f : β → γ
hf : QuasiMeasurePreserving f ν ξ
f' : α → β
hf' : QuasiMeasurePreserving f' μ ν
⊢ ↑g ∘ f ∘ f' =ᵐ[μ] ↑((g.compQuasiMeasurePreserving f hf).compQuasiMeasurePreserving f' hf')
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_4
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace δ
inst✝ : MeasurableSpace β
ν : Measure β
γ : Type u_5
mγ : MeasurableSpace γ
ξ : Measure γ
g : γ →ₘ[ξ] δ
f : β → γ
hf : QuasiMeasurePreserving f ν ξ
f' : α → β
hf' : QuasiMeasurePreserving f' μ ν
⊢ ↑g ∘ f ∘ f' =ᵐ[μ] ↑((g.compQuasiMeasurePreserving f hf).compQuasiMeasurePreserving f' hf')

Tactic:
coeFn_compQuasiMeasurePreserving,

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_4
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace δ
inst✝ : MeasurableSpace β
ν : Measure β
γ : Type u_5
mγ : MeasurableSpace γ
ξ : Measure γ
g : γ →ₘ[ξ] δ
f : β → γ
hf : QuasiMeasurePreserving f ν ξ
f' : α → β
hf' : QuasiMeasurePreserving f' μ ν
⊢ ↑g ∘ f ∘ f' =ᵐ[μ] ↑(g.compQuasiMeasurePreserving f hf) ∘ f'
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_4
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace δ
inst✝ : MeasurableSpace β
ν : Measure β
γ : Type u_5
mγ : MeasurableSpace γ
ξ : Measure γ
g : γ →ₘ[ξ] δ
f : β → γ
hf : QuasiMeasurePreserving f ν ξ
f' : α → β
hf' : QuasiMeasurePreserving f' μ ν
⊢ ↑g ∘ f ∘ f' =ᵐ[μ] ↑(g.compQuasiMeasurePreserving f hf) ∘ f'

Tactic:
coeFn_compQuasiMeasurePreserving,

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_4
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace δ
inst✝ : MeasurableSpace β
ν : Measure β
γ : Type u_5
mγ : MeasurableSpace γ
ξ : Measure γ
g : γ →ₘ[ξ] δ
f : β → γ
hf : QuasiMeasurePreserving f ν ξ
f' : α → β
hf' : QuasiMeasurePreserving f' μ ν
⊢ ↑g ∘ f ∘ f' =ᵐ[μ] (↑g ∘ f) ∘ f'
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
n : ι → ℕ
⊢ (univ.pi fun a ↦ update (fun i' ↦ t i' (n a)) i s a) ∈ univ.pi '' univ.pi C

Tactic:
apply mem_image_of_mem

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
n : ι → ℕ
⊢ (fun a ↦ update (fun i' ↦ t i' (n a)) i s a) ∈ univ.pi C
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
| (Measure.count s)⁻¹ * Measure.count (s ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count s) +
    (Measure.count t)⁻¹ * Measure.count (t ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ t))

Tactic:
Set.union_inter_cancel_right,

Goal state after:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
| (Measure.count s)⁻¹ * Measure.count (s ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count s) +
    (Measure.count t)⁻¹ * Measure.count (t ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count t)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
inst✝ : ENorm ε
μ : Measure α
f : α → ε
hq0_lt : 0 < q
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ = (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q * q)

Tactic:
one_div,

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
inst✝ : ENorm ε
μ : Measure α
f : α → ε
hq0_lt : 0 < q
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ = (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (q⁻¹ * q)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∀ j ∈ Finset.univ,
    j ≠ i → (μ j).toOuterMeasure (eval j '' (t ∩ (fun b ↦ b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)

pp: case refine_3
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∀ j ∈ Finset.univ,
    j ≠ i → (μ j).toOuterMeasure (eval j '' (t \ (fun b ↦ b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)

Tactic:
· rintro j - _; gcongr; apply inter_subset_left

Goal state after:
case refine_3
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∀ j ∈ Finset.univ,
    j ≠ i → (μ j).toOuterMeasure (eval j '' (t \ (fun b ↦ b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (OuterMeasure.pi fun i ↦ (μ i).toOuterMeasure) (univ.pi s) ≤ ∏ i, (μ i) (s i)

Tactic:
apply OuterMeasure.pi_pi_le

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
f : (i : ι) → Set (α i)
s : Finset ι
⊢ (Measure.pi μ) ((↑s).pi f) = ∏ i ∈ s, (μ i) (f i)

Tactic:
simp [← Set.univ_pi_ite, pi_pi, apply_ite]

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

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ 1 / p.toReal * p.toReal = 1

Tactic:
refine one_div_mul_cancel ?_

Goal state after:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ p.toReal ≠ 0
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ ‖c‖ₑ ^ (p.toReal * (1 / p.toReal)) * μ s ^ (1 / p.toReal) = ‖c‖ₑ * μ s ^ (1 / p.toReal)

pp: case hz
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ 0 ≤ 1 / p.toReal

Tactic:
mul_one_div_cancel hp_pos.ne',

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ ‖c‖ₑ ^ 1 * μ s ^ (1 / p.toReal) = ‖c‖ₑ * μ s ^ (1 / p.toReal)

case hz
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ 0 ≤ 1 / p.toReal
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p * p) ≤ ↑c ^ p * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p * p)

Tactic:
one_div,

Goal state after:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (p⁻¹ * p) ≤ ↑c ^ p * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (p⁻¹ * p)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableMul (α i)
inst✝ : ∀ (i : ι), (μ i).IsMulLeftInvariant
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (map (fun x ↦ v * x) (Measure.pi μ)) (univ.pi s) = ∏ i, (μ i) (s i)

Tactic:
map_apply (measurable_const_mul _) (MeasurableSet.univ_pi hs),

Goal state after:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableMul (α i)
inst✝ : ∀ (i : ι), (μ i).IsMulLeftInvariant
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.pi μ) ((fun x ↦ v * x) ⁻¹' univ.pi s) = ∏ i, (μ i) (s i)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
p : ℝ
hp : 0 < p
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p * p) ≤ ↑c ^ p * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p * p)

Tactic:
one_div,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
p : ℝ
hp : 0 < p
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (p⁻¹ * p) ≤ ↑c ^ p * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (p⁻¹ * p)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
hx : x ∈ s
⊢ dist (f x) (g x) ≤ ‖c‖

Tactic:
Real.norm_eq_abs,

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
hx : x ∈ s
⊢ dist (f x) (g x) ≤ |c|
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p * p) ≤ c ^ p * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p * p)

Tactic:
one_div,

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (p⁻¹ * p) ≤ c ^ p * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (p⁻¹ * p)