mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
⊢ affineSpan k (Set.range fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k (Set.range Subtype.val)

Tactic:
apply le_antisymm
    <;> intro q hq
    <;> rw [mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd k V _ (⟨p, hp⟩ : s) q] at hq ⊢
    <;> obtain ⟨t, μ, rfl⟩ := hq
    <;> use t
    <;> [use fun x => μ x * ↑(w x); use fun x => μ x * ↑(w x)⁻¹]
    <;> simp [smul_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
f : ↑(Set.range p) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := ⋯ }
⊢ AffineIndependent k fun x ↦ ↑x

Tactic:
convert! ha.comp_embedding fe

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
f : ↑(Set.range p) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := ⋯ }
x✝ : ↑(Set.range p)
⊢ Subtype.val = p ∘ ⇑fe
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s1 s2 : Set ι
p0 : P
hp0s1 : p0 ∈ affineSpan k (p '' s1)
hp0s2 : p0 ∈ affineSpan k (p '' s2)
hp0' : p0 ∈ affineSpan k (p '' (s1 ∩ s2))
⊢ ∃ i, i ∈ s1 ∩ s2

Tactic:
← Set.Nonempty

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s1 s2 : Set ι
p0 : P
hp0s1 : p0 ∈ affineSpan k (p '' s1)
hp0s2 : p0 ∈ affineSpan k (p '' s2)
hp0' : p0 ∈ affineSpan k (p '' (s1 ∩ s2))
⊢ (s1 ∩ s2).Nonempty
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
hs : s.Finite
⊢ (convexHull R) s = ⇑(∑ x, (LinearMap.proj x).smulRight ↑x) '' stdSimplex R ↑s

Tactic:
let := hs.fintype
  rw [← convexHull_basis_eq_stdSimplex, LinearMap.image_convexHull, ← Set.range_comp]
  apply congr_arg
  aesop

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

Goal state before:
pp: case e_a.e_a
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
i : ι
t : Finset ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
ha : i ∉ t
hw : ∑ j ∈ t, w j ≠ 0
⊢ (w i + ∑ i ∈ t, w i)⁻¹ = 1 / (w i + ∑ i ∈ t, w i)

Tactic:
one_div

Goal state after:
case e_a.e_a
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
i : ι
t : Finset ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
ha : i ∉ t
hw : ∑ j ∈ t, w j ≠ 0
⊢ (w i + ∑ i ∈ t, w i)⁻¹ = (w i + ∑ i ∈ t, w i)⁻¹
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : Group V
inst✝³ : TopologicalSpace V
inst✝² : Torsor V P
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalTorsor P
p : P
v : V
⊢ v⁻¹ = 1 / v

Tactic:
one_div

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : Group V
inst✝³ : TopologicalSpace V
inst✝² : Torsor V P
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalTorsor P
p : P
v : V
⊢ v⁻¹ = v⁻¹
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝ : TopologicalSpace α
⊢ (∀ (x : Set (Set α)), (∀ s ∈ compl '' x, IsOpen[inst✝] s) → IsOpen[inst✝] (⋂₀ (compl '' x))) = ?m.14

Tactic:
forall_mem_image,

Goal state after:
α : Type u_3
inst✝ : TopologicalSpace α
⊢ (∀ (x : Set (Set α)), (∀ ⦃x_1 : Set α⦄, x_1 ∈ x → IsOpen[inst✝] x_1ᶜ) → IsOpen[inst✝] (⋂₀ (compl '' x))) = ?m.14
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case inr.refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = Submodule.span k (⇑(Equiv.vaddConst p).symm '' s)
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ {p} ∪ ⇑(Equiv.vaddConst p) '' b ⊆ s

pp: case inr.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = Submodule.span k (⇑(Equiv.vaddConst p).symm '' s)
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ affineSpan k ({p} ∪ ⇑(Equiv.vaddConst p) '' b) = affineSpan k s

Tactic:
· apply Set.union_subset (Set.singleton_subset_iff.mpr hp)
    rwa [← (Equiv.vaddConst p).subset_symm_image b s]

Goal state after:
case inr.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = Submodule.span k (⇑(Equiv.vaddConst p).symm '' s)
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ affineSpan k ({p} ∪ ⇑(Equiv.vaddConst p) '' b) = affineSpan k s
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∈ s ∧ w i ≠ 0
⊢ ∀ i ∈ s, w i = 0

Tactic:
refine False.elim (hi ?_)
      let wm : ι → k := -(w i)⁻¹ • w
      have hms : s.weightedVSub p wm = (0 : V) := by simp [wm, hs]
      have hwm : ∑ i ∈ s, wm i = 0 := by simp [wm, ← Finset.mul_sum, hw]
      have hwmi : wm i = -1 := by simp [wm, his.2]
      let w' : { y // y ≠ i } → k := fun x => wm x
      have hw' : ∑ x ∈ s', w' x = 1 := by
        simp_rw [w', s', Finset.sum_subtype_eq_sum_filter]
        rw [← s.sum_filter_add_sum_filter_not (· ≠ i)] at hwm
        simpa only [not_not, Finset.filter_eq' _ i, if_pos his.1, sum_singleton, hwmi,
          add_neg_eq_zero] using hwm
      rw [← s.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one hms his.1 hwmi, ←
        (Subtype.range_coe : _ = { x | x ≠ i }), ← Set.range_comp, ←
        s.affineCombination_subtype_eq_filter]
      exact affineCombination_mem_affineSpan hw' p'

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
hf : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : 0 < ∑ i ∈ t, w i
hmem : ∀ i ∈ t, p i ∈ s
⊢ f (t.centerMass w p) ≤ t.centerMass w (f ∘ p)

Tactic:
have hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ { p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2 } := fun i hi =>
    ⟨hmem i hi, le_rfl⟩

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 : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : 0 < ∑ i ∈ t, w i
hmem : ∀ i ∈ t, p i ∈ s
hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ {p | p.1 ∈ s ∧ f p.1 ≤ p.2}
⊢ f (t.centerMass w p) ≤ t.centerMass w (f ∘ p)
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case h
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : s'.Nonempty
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p
⊢ ∑ x ∈ s', (q x).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p

Tactic:
refine (Finset.sum_le_sum hs).trans ?_

Goal state after:
case h
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : s'.Nonempty
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p
⊢ ∑ i ∈ s', s'.sup fC • (s'.biUnion fₛ).sup p ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst✝⁶ : AddCommGroup E
inst✝⁵ : NormedField 𝕝
inst✝⁴ : Module 𝕝 E
inst✝³ : AddCommGroup F
inst✝² : NormedField 𝕝₂
inst✝¹ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝ : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
⊢ Continuous[x✝¹, x✝] ⇑f

Tactic:
refine continuous_of_continuous_comp hq _ fun i => ?_

Goal state after:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst✝⁶ : AddCommGroup E
inst✝⁵ : NormedField 𝕝
inst✝⁴ : Module 𝕝 E
inst✝³ : AddCommGroup F
inst✝² : NormedField 𝕝₂
inst✝¹ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝ : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
⊢ Continuous[x✝¹, _] ⇑((q i).comp f)
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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖f y‖₊⁻¹ * ‖y‖₊ < 1
hy' : ‖y‖₊ ≠ 0
hfy : ‖f y‖₊ ≠ 0
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊

Tactic:
← NNReal.lt_inv_iff_mul_lt hy'

Goal state after:
𝕜 : 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‖₊
y : E
hy : r * ‖f y‖₊⁻¹ < ‖y‖₊⁻¹
hy' : ‖y‖₊ ≠ 0
hfy : ‖f y‖₊ ≠ 0
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: case mpr
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
⊢ (∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K) →
    ∀ (K : Set α),
      IsCompact K →
        ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U

Tactic:
intro h K hK U hU hf
    -- Due to Lebesgue number lemma, there exists an entourage `V`
    -- such that `U` includes the `V`-thickening of `f '' K`.
    rcases lebesgue_number_of_compact_open (hK.image (map_continuous f)) hU hf.image_subset
        with ⟨V, hV, -, hVf⟩
    -- Then any continuous map that is uniformly `V`-close to `f` on `K`
    -- maps `K` to `U` as well
    filter_upwards [h K hK V hV] with g hg x hx using hVf _ (mem_image_of_mem f hx) (hg x hx)

Goal state after:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ ≪ (μ univ)⁻¹ • μ.restrict univ

Tactic:
restrict_univ

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ ≪ (μ univ)⁻¹ • μ
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case inl
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > ↑r, ∀ᶠ (a : α) in f, u a < y
x : ℝ≥0
hx : some x > ↑r
a : α
ha : u a < ↑x
ha₀ : u a ≤ 0
⊢ ENNReal.ofReal (u a) < some x

pp: case inr
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > ↑r, ∀ᶠ (a : α) in f, u a < y
x : ℝ≥0
hx : some x > ↑r
a : α
ha : u a < ↑x
ha₀ : 0 ≤ u a
⊢ ENNReal.ofReal (u a) < some x

Tactic:
· simpa [ofReal_of_nonpos, *] using hx.bot_lt

Goal state after:
case inr
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > ↑r, ∀ᶠ (a : α) in f, u a < y
x : ℝ≥0
hx : some x > ↑r
a : α
ha : u a < ↑x
ha₀ : 0 ≤ u a
⊢ ENNReal.ofReal (u a) < some x
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : TopologicalSpace α
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
inst✝¹ : Field 𝕜
inst✝ : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x : α
⊢ ∃ f ∈ ↑s, f x = v x ∧ f x = v x

Tactic:
exact ⟨_, (v x • (1 : s) : s).prop, mul_one _, mul_one _⟩

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ s, MeasurableSet s ∧ μ s < ∞ ∧ eLpNorm (sᶜ.indicator f) p μ < ε

Tactic:
rcases eq_or_ne p 0 with rfl | hp₀

Goal state after:
case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : NormedAddCommGroup β
f : α → β
ε : ℝ≥0∞
hε : ε ≠ 0
hp_top : 0 ≠ ∞
hf : MemLp f 0 μ
⊢ ∃ s, MeasurableSet s ∧ μ s < ∞ ∧ eLpNorm (sᶜ.indicator f) 0 μ < ε

case inr
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
⊢ ∃ s, MeasurableSet s ∧ μ s < ∞ ∧ eLpNorm (sᶜ.indicator f) p μ < ε
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X
this : (piPremeasure fun i ↦ (μ i).toOuterMeasure) = ⇑(Measure.map (⇑e.symm) (μ default))
⊢ Measure.map (⇑e) ((boundedBy ⇑(Measure.map (⇑e.symm) (μ default)).toOuterMeasure).toMeasure ⋯) = μ default

Tactic:
boundedBy_eq_self,

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X
this : (piPremeasure fun i ↦ (μ i).toOuterMeasure) = ⇑(Measure.map (⇑e.symm) (μ default))
⊢ Measure.map (⇑e) ((Measure.map (⇑e.symm) (μ default)).toMeasure ⋯) = μ default
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = ‖g x‖ₑ
⊢ eLpNorm' f q μ = eLpNorm' g q μ

Tactic:
have : (‖f ·‖ₑ ^ q) =ᵐ[μ] (‖g ·‖ₑ ^ q) := hfg.mono fun x hx ↦ by simp [hx]
  simp only [eLpNorm'_eq_lintegral_enorm, lintegral_congr_ae this]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ ν : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hq : 0 ≤ q
⊢ eLpNorm' f q ν ≤ eLpNorm' f q μ

Tactic:
by
  simp_rw [eLpNorm']
  gcongr

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

Goal state before:
pp: case e_a.e_a
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
⊢ 1 / p.toReal = (1 / p).toReal

Tactic:
one_div

Goal state after:
case e_a.e_a
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
⊢ p.toReal⁻¹ = p⁻¹.toReal
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ 1 + (p - 1)⁻¹ = 1 + 1 / (p - 1)

Tactic:
one_div

Goal state after:
p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ 1 + (p - 1)⁻¹ = 1 + (p - 1)⁻¹
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
⊢ p * y ^ (p - 1) < (z ^ p - y ^ p) / (z - y)

Tactic:
have q : 0 < z - y := by rwa [sub_pos]
    rw [lt_div_iff₀ q, ← div_lt_div_iff_of_pos_right hy', _root_.sub_div, div_self hy'.ne',
      ← div_rpow hz hy.le, lt_sub_iff_add_lt', ← add_sub_cancel_right (z / y) 1, add_comm _ 1,
      add_sub_assoc, ← div_mul_eq_mul_div, mul_div_assoc, ← rpow_sub hy, sub_sub_cancel_left,
      rpow_neg_one, mul_assoc, ← div_eq_inv_mul, _root_.sub_div, div_self hy.ne']
    apply one_add_mul_self_lt_rpow_one_add _ _ hp
    · rw [le_sub_iff_add_le, neg_add_cancel, div_nonneg_iff]
      exact Or.inl ⟨hz, hy.le⟩
    · rw [sub_ne_zero]
      exact ((one_lt_div hy).mpr hyz).ne'

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ∞
hbdd : ∀ (n : ℕ), (∫⁻ (x : α), ‖f n x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≤ ↑R
⊢ liminf (fun i ↦ ∫⁻ (a : α), ↑‖f i a‖₊ ^ p.toReal ∂μ) atTop ≤ ↑R ^ p.toReal

Tactic:
one_div

Goal state after:
case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ∞
hbdd : ∀ (n : ℕ), (∫⁻ (x : α), ‖f n x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ ≤ ↑R
⊢ liminf (fun i ↦ ∫⁻ (a : α), ↑‖f i a‖₊ ^ p.toReal ∂μ) atTop ≤ ↑R ^ p.toReal
Module: Mathlib.Analysis.Convex.Mul

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁷ : CommRing 𝕜
inst✝¹⁶ : LinearOrder 𝕜
inst✝¹⁵ : IsStrictOrderedRing 𝕜
inst✝¹⁴ : CommRing E
inst✝¹³ : LinearOrder E
inst✝¹² : IsStrictOrderedRing E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : LinearOrder F
inst✝⁹ : IsOrderedAddMonoid F
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜 G
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
inst✝⁴ : Module E F
inst✝³ : IsScalarTower 𝕜 E F
inst✝² : SMulCommClass 𝕜 E F
inst✝¹ : IsOrderedModule 𝕜 F
inst✝ : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * a) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g x + f y • g y) =
    (a * (a + b)) • f x • g x + (b * (a + b)) • f y • g y

Tactic:
simp only [mul_add, add_smul, smul_add, mul_comm _ a]; abel

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁸ : CommRing 𝕜
inst✝¹⁷ : LinearOrder 𝕜
inst✝¹⁶ : IsStrictOrderedRing 𝕜
inst✝¹⁵ : CommRing E
inst✝¹⁴ : LinearOrder E
inst✝¹³ : IsStrictOrderedRing E
inst✝¹² : AddCommGroup F
inst✝¹¹ : LinearOrder F
inst✝¹⁰ : IsOrderedAddMonoid F
inst✝⁹ : AddCommGroup G
inst✝⁸ : Module 𝕜 G
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : IsOrderedModule 𝕜 F
inst✝¹ : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
inst✝ : IsOrderedModule 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * (a + b)) • f x • g x + (b * (a + b)) • f y • g y =
    (a * a) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g x + f y • g y)

Tactic:
simp only [mul_add, add_smul, smul_add, mul_comm _ a]; abel

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

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

Tactic:
one_div

Goal state after:
case inr
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ = 0

Tactic:
rw [← @lintegral_zero_fun α _ μ]
  refine lintegral_congr_ae ?_
  suffices h_mul_zero : f * g =ᵐ[μ] 0 * g by rwa [zero_mul] at h_mul_zero
  have hf_eq_zero : f =ᵐ[μ] 0 := ae_eq_zero_of_lintegral_rpow_eq_zero hp0 hf hf_zero
  exact hf_eq_zero.mul (ae_eq_refl g)

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ∞
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ∞
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
· exact lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top hpq.pos hpq.symm.nonneg hf_top hg_zero

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ∞
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)