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

Goal state before:
pp: case neg.convert_3.inr
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
i : E
h✝ : i = y
⊢ i ∈ s

Tactic:
subst i

Goal state after:
case neg.convert_3.inr
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ y ∈ s
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
Y : Type u_4
f : X → Y
⊢ LocallyPathConnectedSpace Y

Tactic:
let _ := TopologicalSpace.coinduced f ‹_›

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
⊢ LocallyPathConnectedSpace Y
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case refine_1
X✝ : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
x✝ y z : X✝
ι : Type u_3
F : Set X✝
inst✝² : LocallyPathConnectedSpace X✝
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ mk x.fst '' pathComponentIn (mk x.fst ⁻¹' u) x.snd ⊆ pathComponentIn u x

pp: case refine_2
X✝ : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
x✝ y z : X✝
ι : Type u_3
F : Set X✝
inst✝² : LocallyPathConnectedSpace X✝
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ IsOpen[instTopologicalSpaceSigma] (mk x.fst '' pathComponentIn (mk x.fst ⁻¹' u) x.snd)

pp: case refine_3
X✝ : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
x✝ y z : X✝
ι : Type u_3
F : Set X✝
inst✝² : LocallyPathConnectedSpace X✝
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ x ∈ mk x.fst '' pathComponentIn (mk x.fst ⁻¹' u) x.snd

Tactic:
· apply IsPathConnected.subset_pathComponentIn
    · exact (isPathConnected_pathComponentIn (by exact hxu)).image continuous_sigmaMk
    · exact ⟨x.2, mem_pathComponentIn_self hxu, rfl⟩
    · exact (image_mono pathComponentIn_subset).trans (u.image_preimage_subset _)

Goal state after:
case refine_2
X✝ : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
x✝ y z : X✝
ι : Type u_3
F : Set X✝
inst✝² : LocallyPathConnectedSpace X✝
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ IsOpen[instTopologicalSpaceSigma] (mk x.fst '' pathComponentIn (mk x.fst ⁻¹' u) x.snd)

case refine_3
X✝ : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
x✝ y z : X✝
ι : Type u_3
F : Set X✝
inst✝² : LocallyPathConnectedSpace X✝
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ x ∈ mk x.fst '' pathComponentIn (mk x.fst ⁻¹' u) x.snd
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
⊢ (convexHull R) (Set.range v) = {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x}

Tactic:
refine Subset.antisymm (convexHull_min ?_ ?_) ?_
  · intro x hx
    obtain ⟨i, hi⟩ := Set.mem_range.mp hx
    exact ⟨{i}, Function.const ι (1 : R), by simp, by simp, by simp [hi]⟩
  · rintro x ⟨s, w, hw₀, hw₁, rfl⟩ y ⟨s', w', hw₀', hw₁', rfl⟩ a b ha hb hab
    let W : ι → R := fun i => (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
    have hW₁ : (s ∪ s').sum W = 1 := by
      rw [sum_add_distrib, ← sum_subset subset_union_left,
        ← sum_subset subset_union_right, sum_ite_of_true,
        sum_ite_of_true, ← mul_sum, ← mul_sum, hw₁, hw₁', ← add_mul, hab,
        mul_one] <;> intros <;> simp_all
    refine ⟨s ∪ s', W, ?_, hW₁, ?_⟩
    · rintro i -
      by_cases hi : i ∈ s <;> by_cases hi' : i ∈ s' <;>
        simp [W, hi, hi', add_nonneg, mul_nonneg ha (hw₀ i _), mul_nonneg hb (hw₀' i _)]
    · simp_rw [W, affineCombination_eq_linear_combination (s ∪ s') v _ hW₁,
        affineCombination_eq_linear_combination s v w hw₁,
        affineCombination_eq_linear_combination s' v w' hw₁', add_smul, sum_add_distrib]
      rw [← sum_subset subset_union_left, ← sum_subset subset_union_right]
      · simp only [ite_smul, sum_ite_of_true fun _ hi => hi, mul_smul, ← smul_sum]
      · intro i _ hi'
        simp [hi']
      · intro i _ hi'
        simp [hi']
  · rintro x ⟨s, w, hw₀, hw₁, rfl⟩
    exact affineCombination_mem_convexHull hw₀ hw₁

Goal state after:
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset E
wx : E → R
hwx₀ : ∀ y ∈ s, 0 ≤ wx y
hwx₁ : ∑ y ∈ s, wx y = 1
wy : E → R
hwy₀ : ∀ y ∈ s, 0 ≤ wy y
hwy₁ : ∑ y ∈ s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∀ y ∈ s, 0 ≤ a * wx y + b * wy y

Tactic:
rintro i hi
      apply_rules [add_nonneg, mul_nonneg, hwx₀, hwy₀]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
⊢ Bornology.IsBounded ((convexHull ℝ) s) ↔ Bornology.IsBounded s

Tactic:
by
  simp only [isBounded_iff_ediam_ne_top, convexHull_ediam]

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

Goal state before:
pp: case pos
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : x ≠ 0
⊢ ∃ V ∈ p.addGroupFilterBasis.sets, V ⊆ (fun y ↦ x • y) ⁻¹' (s.sup p).ball 0 r

Tactic:
rw [(s.sup p).smul_ball_preimage 0 r x h, smul_zero]

Goal state after:
case pos
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : x ≠ 0
⊢ ∃ V ∈ p.addGroupFilterBasis.sets, V ⊆ (s.sup p).ball 0 (r / ‖x‖)
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ WithSeminorms fun p ↦ ↑p

Tactic:
by
    have := hp.topologicalAddGroup
    have hp' (i : ι) : Continuous (p i) := hp.continuous_seminorm i
    rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf] at ⊢ hp
    refine le_antisymm ?_ ?_
    · simp_rw [le_iInf_iff, ← tendsto_iff_comap]
      intro ⟨p, hp⟩
      exact hp.tendsto' 0 0 (map_zero _)
    · simp_rw [hp, le_iInf_iff]
      intro i
      exact iInf_le (ι := {p : Seminorm 𝕜 E // Continuous p}) _ ⟨p i, hp' i⟩

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 ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r) → ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r

Tactic:
intro hI i
    convert! hI { i }
    rw [Finset.sup_singleton]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : ↑r < ‖f‖
hr₀ : ¬↑r < 0
⊢ ∃ x, ‖x‖ < 1 ∧ ↑r < ‖f x‖

Tactic:
exact f.exists_lt_apply_of_lt_opNNNorm hr

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : DenselyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
r : ℝ≥0
hr✝ : r < ‖f‖₊
x : E
hlt : ‖x‖₊ < 1
hr : r < ‖f x‖₊
hx0 : 0 < ‖x‖₊
⊢ 1⁻¹ * ‖f x‖₊ < ‖x‖₊⁻¹ * ‖f x‖₊

Tactic:
by gcongr; exact hr.pos

Goal state after:
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
c₁ c₂ : M
f✝ : l.Germ β
f : α → β
⊢ (c₁ * c₂) • ↑f = c₁ • c₂ • ↑f

Tactic:
by
      norm_cast
      simp [mul_smul]

Goal state after:
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
c₁✝ c₂✝ : l.Germ M
f✝ : l.Germ β
c₁ c₂ : α → M
f : α → β
⊢ (↑c₁ * ↑c₂) • ↑f = ↑c₁ • ↑c₂ • ↑f

Tactic:
by
      norm_cast
      simp [mul_smul]

Goal state after:
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝³ : TopologicalSpace α
inst✝² : UniformSpace β
X : Type u_1
inst✝¹ : TopologicalSpace X
f : X → α → β
s : Set α
hf : ∀ (x : X), ContinuousOn (f x) s
inst✝ : CompactSpace ↑s
⊢ (Continuous[inst✝¹, _] fun x ↦ { toFun := s.domRestrict (f x), continuous_toFun := ⋯ }) ↔
    Continuous[inst✝¹, topologicalSpace α β {s}] fun x ↦ (ofFun {s}) (f x)

Tactic:
rw [ContinuousMap.continuous_iff_continuous_uniformFun, UniformOnFun.continuous_rng_iff]
  simp [Function.comp_def]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁵ : NormedField 𝕜₁
inst✝¹⁴ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E✝ : Type u_3
F✝ : Type u_4
G : Type u_5
inst✝¹³ : AddCommGroup E✝
inst✝¹² : Module 𝕜₁ E✝
inst✝¹¹ : TopologicalSpace E✝
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜₂ F✝
𝕜 : Type u_6
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
i : ι
⊢ Continuous[instTopologicalSpace (RingHom.id 𝕜) ((i : ι) → F i) 𝔖, instTopologicalSpace (RingHom.id 𝕜) (F i) 𝔖] fun a ↦
    ContinuousLinearMap.proj i ∘SL a

Tactic:
exact (ContinuousLinearMap.proj i : (Π j, F j) →L[𝕜] F i).postcompUniformConvergenceCLM 𝔖
        |>.continuous

Goal state after:
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case pos
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
c : ℝ
⊢ (∀ y < c, ∀ᶠ (a : ι) in f, y < ↑(u a)) ↔ ∀ y < c.toNNReal, ∀ᶠ (a : ι) in f, y < u a

Tactic:
simp only [← coe_lt_coe, Real.coe_toNNReal', lt_sup_iff, or_imp, isEmpty_Prop, not_lt,
    zero_le_coe, IsEmpty.forall_iff, and_true, NNReal.forall, coe_mk, forall_comm (α := _ ≤ _)]

Goal state after:
case pos
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
c : ℝ
⊢ (∀ y < c, ∀ᶠ (a : ι) in f, y < ↑(u a)) ↔ ∀ x < c, 0 ≤ x → ∀ᶠ (a : ι) in f, x < ↑(u a)
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case pos
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf✝ : f.NeBot
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
c : ℝ
⊢ (∀ y < c, ∃ᶠ (a : ι) in f, y < ↑(u a)) ↔ ∀ y < c.toNNReal, ∃ᶠ (a : ι) in f, y < u a

Tactic:
simp only [← coe_lt_coe, Real.coe_toNNReal', lt_sup_iff, or_imp, isEmpty_Prop, not_lt,
    zero_le_coe, IsEmpty.forall_iff, and_true, NNReal.forall, coe_mk, forall_comm (α := _ ≤ _)]

Goal state after:
case pos
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf✝ : f.NeBot
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
c : ℝ
⊢ (∀ y < c, ∃ᶠ (a : ι) in f, y < ↑(u a)) ↔ ∀ x < c, 0 ≤ x → ∃ᶠ (a : ι) in f, x < ↑(u a)
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
⊢ liminf (fun x ↦ a * u x) f = a * liminf u f

Tactic:
by
  by_cases ha₀ : a = 0
  · simp_rw [ha₀, zero_mul, ← ENNReal.bot_eq_zero]
    apply liminf_const
  exact liminf_const_mul_of_ne_zero_of_ne_top ha₀ ha_top

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : IsTopologicalGroup β
this✝ : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
f : C(α, β)
⊢ ContinuousAt (fun a ↦ a⁻¹) f

Tactic:
rw [ContinuousAt, tendsto_iff_forall_isCompact_tendstoUniformlyOn]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : IsTopologicalGroup β
this✝ : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
f : C(α, β)
⊢ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ i⁻¹ a) (⇑f⁻¹) (nhds f) K
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
s : Set Ω
hs : MeasurableSet s
⊢ uniformOn s = 0 ↔ s.Infinite ∨ s = ∅

Tactic:
simp [uniformOn, hs]

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_2
inst✝ : DecidableEq Ω
x✝ : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet ↑s
ht : MeasurableSet ↑t
⊢ (↑(#s))⁻¹ * ↑(#(s ∩ t)) = ↑(#(s ∩ t)) / ↑(#s)

pp: Ω : Type u_2
inst✝ : DecidableEq Ω
x✝ : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet ↑s
ht : MeasurableSet ↑t
⊢ MeasurableSet ↑(s ∩ t)

Tactic:
· rw [div_eq_mul_inv, mul_comm]

Goal state after:
Ω : Type u_2
inst✝ : DecidableEq Ω
x✝ : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet ↑s
ht : MeasurableSet ↑t
⊢ MeasurableSet ↑(s ∩ t)
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: case inl.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
t u : Set Ω
ht : t.Finite
hs : ∅.Finite
hst : Disjoint ∅ t
ht' : t.Nonempty
⊢ (uniformOn ∅) u * (uniformOn (∅ ∪ t)) ∅ + (uniformOn t) u * (uniformOn (∅ ∪ t)) t = (uniformOn (∅ ∪ t)) u

Tactic:
simp [uniformOn_self ht ht']

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: case inr.inr
Ω : 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 ∪ t) ∩ s)) +
      (Measure.count t)⁻¹ * Measure.count (t ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ t)) =
    (Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ u)

Tactic:
conv_lhs =>
    rw [Set.union_inter_cancel_left, Set.union_inter_cancel_right,
      mul_comm (Measure.count (s ∪ t))⁻¹, mul_comm (Measure.count (s ∪ t))⁻¹, ← mul_assoc,
      ← mul_assoc, mul_comm _ (Measure.count s), mul_comm _ (Measure.count t), ← mul_assoc,
      ← mul_assoc]

Goal state after:
case inr.inr
Ω : 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)⁻¹ * Measure.count (s ∩ u) * (Measure.count (s ∪ t))⁻¹ +
      Measure.count t * (Measure.count t)⁻¹ * Measure.count (t ∩ u) * (Measure.count (s ∪ t))⁻¹ =
    (Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ u)
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 ∂μ ≤ ↑c ^ p * ∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ

Tactic:
enorm,

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 ∂μ ≤ ↑c ^ p * ∫⁻ (a : α), ↑‖g a‖₊ ^ p ∂μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
s : Set α
f g : α → ε
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
⊢ essSup (fun x ↦ ‖s.piecewise f g x‖ₑ) μ = essSup (s.piecewise (fun x ↦ ‖f x‖ₑ) fun x ↦ ‖g x‖ₑ) μ

Tactic:
congr with x

Goal state after:
case e_f
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
s : Set α
f g : α → ε
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
x : α
⊢ ‖s.piecewise f g x‖ₑ = s.piecewise (fun x ↦ ‖f x‖ₑ) (fun x ↦ ‖g x‖ₑ) x
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
hp0_lt : 0 < q
⊢ eLpNorm' 0 q μ = 0

Tactic:
by
  simp [eLpNorm'_eq_lintegral_enorm, hp0_lt]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : Fintype ι'
f : ι' ≃ ι
⊢ Measure.map (⇑(MeasurableEquiv.piCongrLeft α f)) (Measure.pi fun i' ↦ μ (f i')) = Measure.pi μ

Tactic:
refine (pi_eq fun s _ => ?_).symm

Goal state after:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : Fintype ι'
f : ι' ≃ ι
s : (i : ι) → Set (α i)
x✝ : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.map (⇑(MeasurableEquiv.piCongrLeft α f)) (Measure.pi fun i' ↦ μ (f i'))) (univ.pi s) = ∏ i, (μ i) (s i)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
X : ι ⊕ ι' → Type u_4
m : (i : ι ⊕ ι') → MeasurableSpace (X i)
μ : (i : ι ⊕ ι') → Measure (X i)
inst✝ : ∀ (i : ι ⊕ ι'), SigmaFinite (μ i)
⊢ Measure.map (⇑(MeasurableEquiv.sumPiEquivProdPi X).symm)
      ((Measure.pi fun i ↦ μ (Sum.inl i)).prod (Measure.pi fun i ↦ μ (Sum.inr i))) =
    Measure.pi μ

Tactic:
refine (pi_eq fun s _ => ?_).symm

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
X : ι ⊕ ι' → Type u_4
m : (i : ι ⊕ ι') → MeasurableSpace (X i)
μ : (i : ι ⊕ ι') → Measure (X i)
inst✝ : ∀ (i : ι ⊕ ι'), SigmaFinite (μ i)
s : (i : ι ⊕ ι') → Set (X i)
x✝ : ∀ (i : ι ⊕ ι'), MeasurableSet (s i)
⊢ (Measure.map (⇑(MeasurableEquiv.sumPiEquivProdPi X).symm)
        ((Measure.pi fun i ↦ μ (Sum.inl i)).prod (Measure.pi fun i ↦ μ (Sum.inr i))))
      (univ.pi s) =
    ∏ i, (μ i) (s i)
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 : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
⊢ (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ

Tactic:
by_cases hp' : p = ⊤

Goal state after:
case pos
α : 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 : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
hp' : p = ∞
⊢ (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ

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 : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
hp' : ¬p = ∞
⊢ (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f z - f y) / (z - y) < (f y - f x) / (y - x)

Tactic:
by
  have := StrictConvexOn.slope_strict_mono_adjacent hf.neg hx hz hxy hyz
  simp only [Pi.neg_apply] at this
  linear_combination this

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑C
⊢ eLpNorm f ∞ μ < ∞

Tactic:
rw [eLpNorm_exponent_top]
    exact eLpNormEssSup_lt_top_of_ae_enorm_bound hfC

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

Goal state before:
pp: p q : ℝ
h : p.HolderConjugate q
⊢ ENNReal.ofReal (p⁻¹ + q⁻¹) = ENNReal.ofReal 1

Tactic:
h.inv_add_inv_eq_one

Goal state after:
p q : ℝ
h : p.HolderConjugate q
⊢ ENNReal.ofReal 1 = ENNReal.ofReal 1
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q r : ℝ≥0
h : p.HolderTriple q r
⊢ r⁻¹ - q⁻¹ = p⁻¹

Tactic:
by
  have := h.symm.inv_lt_inv.le
  exact_mod_cast h.coe.inv_sub_inv_eq_inv

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
⊢ eLpNorm f p μ' < ∞

Tactic:
eLpNorm_le_of_measure_le_smul hμ'_le

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
⊢ c ^ (1 / p).toReal • eLpNorm f p μ < ∞