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

Goal state before:
pp: case 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 : Set E
⊢ s ⊆ {x | ∃ ι t w z, (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x}

Tactic:
intro x hx

Goal state after:
case 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 : Set E
x : E
hx : x ∈ s
⊢ x ∈ {x | ∃ ι t w z, (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x}
Module: Mathlib.Topology.Algebra.Module.LocallyConvex

Goal state before:
pp: case inl.refine_2
R : Type u_1
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
x : R
hl : IsBot x
inst✝ : OrderBot R
⊢ ∀ (i' : Set R), i' ∈ 𝓝 ⊥ ∧ Convex R i' → id i' ∈ 𝓝 ⊥

Tactic:
simp +contextual

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

Goal state before:
pp: case inr.inl.refine_2
R : Type u_1
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
x : R
hl : ∃ b, b < x
hu : IsTop x
inst✝ : OrderTop R
⊢ ∀ (i' : Set R), i' ∈ 𝓝 ⊤ ∧ Convex R i' → id i' ∈ 𝓝 ⊤

Tactic:
simp +contextual

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

Goal state before:
pp: case inr.inr.refine_2
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : OrderTopology R
x : R
hl : ∃ b, b < x
hu : ∃ b, x < b
⊢ ∀ (i' : Set R), i' ∈ 𝓝 x ∧ Convex R i' → id i' ∈ 𝓝 x

Tactic:
simp +contextual

Goal state after:
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
v : 𝕜
q : E
hf : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : v + ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
hv : 0 ≤ v
hq : q ∈ s
W : Option ι → 𝕜 := fun j ↦ j.elim v w
P : Option ι → E := fun j ↦ j.elim q p
⊢ f (v • q + ∑ i ∈ t, w i • p i) ≤ v • f q + ∑ i ∈ t, w i • f (p i)

Tactic:
have : f (∑ j ∈ insertNone t, W j • P j) ≤ ∑ j ∈ insertNone t, W j • f (P j) :=
    hf.map_sum_le (forall_mem_insertNone.2 ⟨hv, h₀⟩) (by simpa using! h₁)
      (forall_mem_insertNone.2 ⟨hq, hmem⟩)

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
v : 𝕜
q : E
hf : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : v + ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
hv : 0 ≤ v
hq : q ∈ s
W : Option ι → 𝕜 := fun j ↦ j.elim v w
P : Option ι → E := fun j ↦ j.elim q p
this : f (∑ j ∈ insertNone t, W j • P j) ≤ ∑ j ∈ insertNone t, W j • f (P j)
⊢ f (v • q + ∑ i ∈ t, w i • p i) ≤ v • f q + ∑ i ∈ t, w i • f (p i)
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case 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
⊢ ↑s ⊆ {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}

Tactic:
intro x hx

Goal state after:
case 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
x : E
hx : x ∈ ↑s
⊢ x ∈ {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}
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
⊢ 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:
have :
      f (∑ i ∈ t with w i ≠ 0, w i • p i) < ∑ i ∈ t with w i ≠ 0, w i • f (p i) ↔
        ∃ j ∈ {x ∈ t | w x ≠ 0}, p j ≠ ∑ i ∈ t with w i ≠ 0, w i • p i :=
    hf.map_sum_lt_iff_of_pos' (by grind)
      (sum_filter_ne_zero _ |>.trans h₁) (hmem _ <| mem_of_mem_filter · ·)
  grind [sum_filter_of_ne, left_ne_zero_of_smul]

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

Goal state before:
pp: case refine_1
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
⊢ p.moduleFilterBasis.filter ≤ comap (⇑(p i)) (𝓝 0)

Tactic:
rw [p.moduleFilterBasis.toFilterBasis.hasBasis.le_basis_iff
        (Metric.nhds_basis_ball.comap _)]

Goal state after:
case refine_1
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
⊢ ∀ (i' : ℝ), 0 < i' → ∃ i_1 ∈ p.moduleFilterBasis.toFilterBasis, id i_1 ⊆ ⇑(p i) ⁻¹' Metric.ball 0 i'
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
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
𝔖 : Set (Set E)
⊢ instTopologicalSpace σ F 𝔖 =
    (UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.uniformSpace E F 𝔖)).toTopologicalSpace

Tactic:
rw [UniformConvergenceCLM.instTopologicalSpace, IsUniformAddGroup.rightUniformSpace_eq]

Goal state after:
𝕜₁ : 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
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
𝔖 : Set (Set E)
⊢ TopologicalSpace.induced DFunLike.coe (UniformOnFun.topologicalSpace E F 𝔖) =
    (UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.uniformSpace E F 𝔖)).toTopologicalSpace
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 : ℝ
hr : r > 0
a : 𝕜
h : s ⊆ (I.sup p).ball 0 ‖a‖
ha : r < ‖a‖
⊢ ∀ x ∈ s, (I.sup p) x < ‖a‖

Tactic:
intro x hx

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
a : 𝕜
h : s ⊆ (I.sup p).ball 0 ‖a‖
ha : r < ‖a‖
x : E
hx : x ∈ s
⊢ (I.sup p) x < ‖a‖
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
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
R : Type u_6
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Module R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (E →SLᵤ[σ, 𝔖] F)
h : ∀ s ∈ 𝔖, IsVonNBounded R (image2 (fun f x ↦ f x) S s)
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
c : R
hc : image2 (fun f x ↦ f x) S s ⊆ c • U
hc₀ : c ≠ 0
f : E →SLᵤ[σ, 𝔖] F
hf : f ∈ S
⊢ c⁻¹ • f ∈ {f | MapsTo (⇑f) s U}

Tactic:
intro x hx

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
R : Type u_6
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Module R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (E →SLᵤ[σ, 𝔖] F)
h : ∀ s ∈ 𝔖, IsVonNBounded R (image2 (fun f x ↦ f x) S s)
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
c : R
hc : image2 (fun f x ↦ f x) S s ⊆ c • U
hc₀ : c ≠ 0
f : E →SLᵤ[σ, 𝔖] F
hf : f ∈ S
x : E
hx : x ∈ s
⊢ (c⁻¹ • f) x ∈ U
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
F : Type u_7
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑q
⊢ ∃ C, 0 < C ∧ ∀ (x : F), q x ≤ C * ‖x‖

Tactic:
by
  have hq' : Tendsto q (𝓝 0) (𝓝 0) := map_zero q ▸ hq.tendsto 0
  rcases NormedAddGroup.nhds_zero_basis_norm_lt.mem_iff.mp (hq' <| Iio_mem_nhds one_pos)
    with ⟨ε, ε_pos, hε⟩
  rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
  have : 0 < ‖c‖ / ε := by positivity
  refine ⟨‖c‖ / ε, this, fun x ↦ ?_⟩
  by_cases hx : ‖x‖ = 0
  · rw [hx, mul_zero]
    exact le_of_eq (map_eq_zero_of_norm_eq_zero q hq hx)
  · refine (normSeminorm 𝕜 F).bound_of_shell q ε_pos hc (fun x hle hlt ↦ ?_) hx
    refine (le_of_lt <| show q x < _ from hε hlt).trans ?_
    rwa [← div_le_iff₀' this, one_div_div]

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

Goal state before:
pp: 𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : RingHomIsometric σ₁₂
inst✝¹ : TopologicalSpace F
inst✝ : PolynormableSpace 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
x✝ : TopologicalSpace E := TopologicalSpace.induced (⇑f) inferInstance
⊢ PolynormableSpace 𝕜 E

Tactic:
exact f.withSeminorms_induced (PolynormableSpace.withSeminorms 𝕜₂ F) |>.toPolynormableSpace

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✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c : M
f✝ g✝ : l.Germ N
f g : α → N
⊢ c • (f + g) =ᶠ[l] c • f + c • g

Tactic:
simp [smul_add]

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✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c✝ : l.Germ M
f✝ g✝ : l.Germ N
c : α → M
f g : α → N
⊢ c • (f + g) =ᶠ[l] c • f + c • g

Tactic:
simp [smul_add]

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

Goal state before:
pp: ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ᶠ (a : ι) in f, ↑(u a) ≤ b
⊢ ∀ (a : ι), ↑(u a) ≤ b → ↑(u a) ≤ ↑b.toNNReal

Tactic:
simp +contextual

Goal state after:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
⊢ ∑ x, μ (X ⁻¹' {x} ∩ E) = μ E

Tactic:
have : ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E := by ext; simp
      rw [← measure_biUnion_finset _ fun _ _ ↦ (hX (.singleton _)).inter hE, this]
      aesop (add simp [PairwiseDisjoint, Set.Pairwise, Function.onFun, disjoint_left])

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

Goal state before:
pp: case inr
α : Type u_1
inst✝⁴ : TopologicalSpace α
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalSemiring R
inst✝ : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h✝ : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
⊢ f ∈ s₁ ↔ f ∈ s₂

Tactic:
have h : f = algebraMap R C(α, R) (f default) := by
        ext x'
        simp only [mul_one, smul_eq_mul, algebraMap_apply]
        congr
        simp [eq_iff_true_of_subsingleton]

Goal state after:
case inr
α : Type u_1
inst✝⁴ : TopologicalSpace α
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalSemiring R
inst✝ : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h✝ : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
h : f = (algebraMap R C(α, R)) (f default)
⊢ f ∈ s₁ ↔ f ∈ s₂
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ω ∉ t
⊢ Measure.count ({ω} ∩ t) = 0

Tactic:
· simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ → δ
hg : Continuous[instTopologicalSpaceProd, inst✝²] (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ ↑(comp₂ g hg f₁ f₂) =ᵐ[μ] fun a ↦ g (↑f₁ a) (↑f₂ a)

Tactic:
rw [comp₂_eq_mk]
  apply coeFn_mk

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
⊢ (uniformOn s) (t ∩ u) = (uniformOn (s ∩ t)) u * (uniformOn s) t

Tactic:
by_cases hst : s ∩ t = ∅
  · rw [hst, uniformOn_empty_meas, Measure.coe_zero, Pi.zero_apply, zero_mul,
      uniformOn_eq_zero_iff hs, ← Set.inter_assoc, hst, Set.empty_inter]
  rw [uniformOn, uniformOn, cond_apply hs.measurableSet, cond_apply hs.measurableSet,
    cond_apply (hs.inter_of_left _).measurableSet, mul_comm _ (Measure.count (s ∩ t)),
    ← mul_assoc, mul_comm _ (Measure.count (s ∩ t)), ← mul_assoc, ENNReal.mul_inv_cancel, one_mul,
    mul_comm, Set.inter_assoc]
  · rwa [← Measure.count_eq_zero_iff] at hst
  · exact (Measure.count_apply_lt_top.2 <| hs.inter_of_left _).ne

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)⁻¹ * 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)

Tactic:
rw [ENNReal.mul_inv_cancel, ENNReal.mul_inv_cancel, one_mul, one_mul, ← add_mul, ← measure_union,
    Set.union_inter_distrib_right, mul_comm]

Goal state after:
case inr.inr.hd
Ω : 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
⊢ Disjoint (s ∩ u) (t ∩ u)

case inr.inr.h
Ω : 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
⊢ MeasurableSet (t ∩ u)

case inr.inr.h0
Ω : 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 t ≠ 0

case inr.inr.ht
Ω : 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 t ≠ ⊤

case inr.inr.h0
Ω : 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 ≠ 0

case inr.inr.ht
Ω : 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 ≠ ⊤
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 : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
this : Encodable ι
⊢ (Measure.pi μ) (univ.pi s) = ∏ i, (μ i) (s i)

Tactic:
rw [← pi'_eq_pi, pi'_pi]

Goal state after:
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)
s : (i : ι ⊕ ι') → Set (X i)
x✝ : ∀ (i : ι ⊕ ι'), MeasurableSet (s i)
⊢ ((Measure.pi fun i ↦ μ (Sum.inl i)).prod (Measure.pi fun i ↦ μ (Sum.inr i)))
      (⇑(Equiv.sumPiEquivProdPi X).symm ⁻¹' univ.pi s) =
    ∏ i, (μ i) (s i)

Tactic:
Equiv.sumPiEquivProdPi_symm_preimage_univ_pi,

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.pi fun i ↦ μ (Sum.inl i)).prod (Measure.pi fun i ↦ μ (Sum.inr i)))
      ((univ.pi fun i ↦ s (Sum.inl i)) ×ˢ univ.pi fun i ↦ s (Sum.inr i)) =
    ∏ i, (μ i) (s i)
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case inr.inl.inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : a < y
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)

Tactic:
convert! hf.slope_mono_adjacent hx hy hxa hya using 1
      rw [← neg_div_neg_eq]; simp

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

Goal state before:
pp: case inl
q : ℝ≥0∞
h : ∞.HolderConjugate q
⊢ ∞ * q = ∞ + q

Tactic:
simp [ne_zero q ∞]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_2.mp
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
j : ι
hj : j ∈ s
⊢ ∀ x ∈ s, w x * log (z j) = log (z x) * w x

Tactic:
intro x hx

Goal state after:
case e'_2.mp
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
j : ι
hj : j ∈ s
x : ι
hx : x ∈ s
⊢ w x * log (z j) = log (z x) * w x
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_2.mpr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
j : ι
hj : j ∈ s
⊢ ∀ x ∈ s, w x * z j = w x * z x

Tactic:
intro x hx

Goal state after:
case e'_2.mpr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
j : ι
hj : j ∈ s
x : ι
hx : x ∈ s
⊢ w x * z j = w x * z x
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Tactic:
by
  have h_rpow : ∀ a : ℝ≥0∞, a ^ q = (a ^ p) ^ (q / p) := fun a => by
    rw [← ENNReal.rpow_mul, mul_div_cancel₀ _ hp_pos.ne']
  have h_rpow_add_rpow_le_add :
    ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p := by
    refine rpow_add_rpow_le_add (a ^ p) (b ^ p) ?_
    rwa [one_le_div hp_pos]
  rw [h_rpow a, h_rpow b, one_div p, ENNReal.le_rpow_inv_iff hp_pos, ← ENNReal.rpow_mul, mul_comm,
    mul_one_div]
  rwa [one_div_div] at h_rpow_add_rpow_le_add

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

Goal state before:
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:
have hp1_real : 1 ≤ p.toReal := by
    rwa [← ENNReal.toReal_one, ENNReal.toReal_le_toReal ENNReal.one_ne_top hp_top]

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 = ∞
hp1_real : 1 ≤ p.toReal
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case inr.inl
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hpq : p ≤ ∞
hq0_lt : 0 < ∞
⊢ eLpNorm f p μ ≤ eLpNorm f ∞ μ * μ Set.univ ^ (1 / p.toReal - 1 / ∞.toReal)

pp: case inr.inr
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
hq_top : q ≠ ∞
⊢ eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)

Tactic:
· simp only [_root_.div_zero, one_div, ENNReal.toReal_top, sub_zero]
    obtain rfl | hp_top := eq_or_ne p ∞
    · simp
    rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
    have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_top
    refine (eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ hp_pos).trans (le_of_eq ?_)
    congr
    exact one_div _

Goal state after:
case inr.inr
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
hq_top : q ≠ ∞
⊢ eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)