mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_4
inst✝ : TopologicalSpace X
h : ∀ (x : X) (u : Set X), IsOpen[inst✝] u → IsOpen[inst✝] (pathComponentIn u x)
x : X
s : Set X
⊢ s ∈ 𝓝 x ↔ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
by
    refine ⟨fun hs ↦ ?_, fun ⟨_, ht⟩ ↦ Filter.mem_of_superset ht.1.1 ht.2⟩
    let ⟨u, hu⟩ := mem_nhds_iff.mp hs
    exact ⟨pathComponentIn u x, ⟨(h x u hu.2.1).mem_nhds (mem_pathComponentIn_self hu.2.2),
      isPathConnected_pathComponentIn hu.2.2⟩, pathComponentIn_subset.trans hu.1⟩

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

Goal state before:
pp: E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
⊢ LocallyPathConnectedSpace ↑S

Tactic:
refine ⟨fun x ↦ ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨t, ht⟩ ↦ mem_of_superset ht.1.1 ht.2⟩⟩⟩

Goal state after:
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : ↑S
s : Set ↑S
hs : s ∈ 𝓝 x
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case refine_2
ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
⊢ IsEmpty ((i : ι) → Z i) ∨ (∀ (i : ι), LocallyPathConnectedSpace (Z i)) ∧ {i | ¬PathConnectedSpace (Z i)}.Finite →
    LocallyPathConnectedSpace ((i : ι) → Z i)

Tactic:
rintro (he | ⟨hloc, hfin⟩)
    · exact ⟨he.elim⟩
    · exact locallyPathConnectedSpace_of_finite_not_pathConnectedSpace hfin

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
⊢ LocallyConvexSpace 𝕜 E

Tactic:
let : TopologicalSpace E := t.induced f

Goal state after:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (⇑f) t
⊢ LocallyConvexSpace 𝕜 E
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
this : (convexHull ℝ) (sphere 0 r) = closedBall 0 r
⊢ (convexHull ℝ) (sphere x r) = closedBall x r

Tactic:
by
    rw [← add_zero x, ← vadd_eq_add, ← vadd_sphere, convexHull_vadd,
      this, vadd_closedBall_zero, vadd_eq_add, add_zero]

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

Goal state before:
pp: 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 t₁ t₂ : Finset E
hs : AffineIndependent R Subtype.val
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : ∑ y ∈ t₁, w₁ y = 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : ∑ y ∈ t₂, w₂ y = 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : E → R := fun x ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
⊢ ∑ i ∈ s, w i = 0

Tactic:
simp [w, Finset.inter_eq_right.2, *]

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

Goal state before:
pp: R : Type u_1
E : Type u_6
ι : Type u_9
inst✝² : SeminormedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : SeminormFamily R E ι
U : Set E
⊢ U ∈ p.basisSets ↔ ∃ i r, 0 < r ∧ U = (i.sup p).ball 0 r

Tactic:
simp only [basisSets, mem_iUnion, exists_prop, mem_singleton_iff]

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

Goal state before:
pp: R : Type u_1
E : Type u_6
ι : Type u_9
inst✝² : SeminormedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : SeminormFamily R E ι
U : Set E
hU : U ∈ p.basisSets
⊢ 0 ∈ U

Tactic:
by
  rcases p.basisSets_iff.mp hU with ⟨ι', r, hr, hU⟩
  rw [hU, mem_ball_zero, map_zero]
  exact hr

Goal state after:
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
i : ι
this : IsTopologicalAddGroup E
⊢ Continuous[⨅ i, PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑(p i)

Tactic:
exact continuous_iInf_dom (@continuous_norm _ (p i).toSeminormedAddGroup)

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✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ≥0
hf : ∀ (x : E), ‖x‖₊ = 1 → ‖f x‖₊ ≤ C
x : E
hx : ‖x‖ = 1
⊢ ‖x‖₊ = 1

Tactic:
← NNReal.coe_eq_one

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ≥0
hf : ∀ (x : E), ‖x‖₊ = 1 → ‖f x‖₊ ≤ C
x : E
hx : ‖x‖ = 1
⊢ ↑‖x‖₊ = 1
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 * ‖y‖₊ < ‖f y‖₊
heq : y = 0
⊢ False

Tactic:
by
      simp [heq, nnnorm_zero, map_zero] at hy

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 : α → β
op : β → γ → δ
f f' : α → β
Hf✝ : f ≈ f'
g g' : α → γ
Hg✝ : g ≈ g'
x : α
Hf : f x = f' x
Hg : g x = g' x
⊢ (fun x ↦ op (f x) (g x)) x = (fun x ↦ op (f' x) (g' x)) x

Tactic:
simp only [Hf, Hg]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
lc : Filter γ
g : γ → α
hf : (↑f).IsConstant
hg : Tendsto g lc l
⊢ (↑(f ∘ g)).IsConstant

Tactic:
rcases hf with ⟨b, hb⟩
  exact ⟨b, hb.comp_tendsto hg⟩

Goal state after:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: case inl
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : μ s ≠ ∞
u : Set Ω
a✝ : MeasurableSet u
hst : μ (s ∩ t) = 0
⊢ μ[|s][u | t] = μ[u | s ∩ t]

Tactic:
have : μ (s ∩ t ∩ u) = 0 := measure_mono_null Set.inter_subset_left hst

Goal state after:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : μ s ≠ ∞
u : Set Ω
a✝ : MeasurableSet u
hst : μ (s ∩ t) = 0
this : μ (s ∩ t ∩ u) = 0
⊢ μ[|s][u | t] = μ[u | s ∩ t]
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inst✝ : f.NeBot
⊢ (IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun i ↦ ↑(u i)) ↔ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u

Tactic:
simp only [IsCoboundedUnder, IsCobounded, eventually_map, ← coe_le_coe, NNReal.forall,
    NNReal.exists]
  constructor
  · rintro ⟨b, hb⟩
    exact ⟨b.toNNReal, by simp, fun x _ ↦ by simpa [*] using hb _⟩
  · rintro ⟨b, hb₀, hb⟩
    exact ⟨b, fun x hx ↦ hb _ (hx.exists.choose_spec.trans' (by simp)) hx⟩

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 ∩ u)) t * (uniformOn s) u

Tactic:
by
  rw [← Set.inter_comm]
  exact uniformOn_inter hs

Goal state after:
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
⊢ q ≠ 0

Tactic:
exact hq0_lt.ne'

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
h : ¬ε = ∞
⊢ μ {x | ε ≤ ↑‖f x‖₊} < ∞

Tactic:
exact hℒp.meas_ge_lt_top'_enorm hp_ne_zero hp_ne_top hε (by simp)

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

Goal state before:
pp: ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
this : ⇑e_meas ⁻¹' univ.pi s = (univ.pi fun i ↦ s (some i)) ×ˢ s none
⊢ (map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((Measure.pi fun i ↦ μ (some i)).prod (μ none))) (univ.pi s) =
    ∏ i, (μ i) (s i)

Tactic:
simp only [e_meas, me.map_apply, univ_option, Finset.prod_insertNone, this,
    prod_prod, pi_pi, mul_comm]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
⊢ eLpNorm (f - g) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)

Tactic:
have hs₃ : s.indicator (f - g) = f - g := by
    rw [Set.indicator_eq_self]
    exact (Function.support_sub _ _).trans (Set.union_subset hs₁ hs₂)

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
hs₃ : s.indicator (f - g) = f - g
⊢ eLpNorm (f - g) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
⊢ eLpNorm (f - g) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)

Tactic:
by
  have hs₃ : s.indicator (f - g) = f - g := by
    rw [Set.indicator_eq_self]
    exact (Function.support_sub _ _).trans (Set.union_subset hs₁ hs₂)
  rw [← hs₃]
  exact eLpNorm_indicator_sub_le_of_dist_bdd μ hp hs hc (fun x _ ↦ h x)

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✝ : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
⊢ eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹

Tactic:
rcases eq_zero_or_neZero μ with rfl | hμ
  · simp
  by_cases hp : p = 0
  · simp [hp]
  have : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ ‖C‖ₑ := hfC.mono fun x hx ↦ hx.trans (le_refl C)
  refine (eLpNorm_mono_enorm_ae this).trans_eq ?_
  rw [eLpNorm_const _ hp (NeZero.ne μ), one_div, enorm_eq_self, smul_eq_mul]

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

Goal state before:
pp: p q r : ℝ≥0
hr : r ≠ 0
⊢ (↑p).HolderTriple ↑q ↑r ↔ p.HolderTriple q r

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [NNReal.holderTriple_iff]
    obtain ⟨hp, hq⟩ : p ≠ 0 ∧ q ≠ 0 := by
      constructor
      all_goals
        rintro rfl
        apply hr
        exact_mod_cast (coe_zero ▸ h).unique _ _ r 0
    exact ⟨by exact_mod_cast h.inv_add_inv_eq_inv, hp.bot_lt, hq.bot_lt⟩
  · rw [holderTriple_iff]
    have hp := h.ne_zero
    have hq := h.symm.ne_zero
    exact_mod_cast h.inv_add_inv_eq_inv

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: s : ℝ
hs : -1 ≤ s
p : ℝ
hp1 : 0 ≤ p
hp2 : p ≤ 1
⊢ (1 + s) ^ p ≤ 1 + p * s

Tactic:
rcases eq_or_lt_of_le hp1 with (rfl | hp1)
  · simp
  rcases eq_or_lt_of_le hp2 with (rfl | hp2)
  · simp
  by_cases hs' : s = 0
  · simp [hs']
  exact (rpow_one_add_lt_one_add_mul_self hs hs' hp1 hp2).le

Goal state after:
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
q : 0 < z - y
⊢ 0 ≤ z ∧ 0 ≤ y ∨ z ≤ 0 ∧ y ≤ 0

Tactic:
exact Or.inl ⟨hz, hy.le⟩

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)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : ¬p.toReal = 0
hp : p ≠ 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n ↦ ‖f n x‖ₑ ^ p.toReal) atTop < ∞

Tactic:
have hp' : p ≠ ∞ := fun h => by simp [h] at hp0

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)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n ↦ ‖f n x‖ₑ ^ p.toReal) atTop < ∞
Module: Mathlib.Algebra.Order.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : CommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedMonoid β
s : Set ι
f : ι → α
g : ι → β
⊢ MonovaryOn f g⁻¹ s ↔ AntivaryOn f g s

Tactic:
simpa [MonovaryOn, AntivaryOn] using forall₂_comm

Goal state after:
Module: Mathlib.Algebra.Order.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : CommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedMonoid β
s : Set ι
f : ι → α
g : ι → β
⊢ AntivaryOn f g⁻¹ s ↔ MonovaryOn f g s

Tactic:
simpa [MonovaryOn, AntivaryOn] using forall₂_comm

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3
ι : 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
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
⊢ ∏ i ∈ s, z i ^ w i = ∏ x ∈ s, rexp (log (z x) * w x)

Tactic:
apply prod_congr rfl

Goal state after:
case e'_3
ι : 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
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
⊢ ∀ x ∈ s, z x ^ w x = rexp (log (z x) * w x)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i ∈ s, w i = 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
hwi : w i ≠ 0
⊢ w i * z i = w i * x

Tactic:
hx i hi hwi

Goal state after:
case inr
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i ∈ s, w i = 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
hwi : w i ≠ 0
⊢ w i * x = w i * x
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 * a) • f y • g x + ((a * b) • f x • g y + (b * b) • f y • g y) =
    (a * a) • f x • g x + (b * b) • f y • g y + ((a * b) • f x • g y + (a * b) • f y • g x)

Tactic:
mul_comm b,

Goal state after:
𝕜 : 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 + (a * b) • f y • g x + ((a * b) • f x • g y + (b * b) • f y • g y) =
    (a * a) • f x • g x + (b * b) • f y • g y + ((a * b) • f x • g y + (a * b) • f y • g x)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_1.h₁
ι : 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
⊢ ∏ i ∈ s, z i ^ w i = ∏ x ∈ s, rexp (log (z x) * w x)

Tactic:
apply prod_congr rfl

Goal state after:
case e'_1.h₁
ι : 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
⊢ ∀ x ∈ s, z x ^ w x = rexp (log (z x) * w x)
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
lift a to NNReal using ha

Goal state after:
p b : ℝ
hb : 0 ≤ b
hp1 : 1 ≤ p
a : ℝ≥0
⊢ ↑a ^ p + b ^ p ≤ (↑a + b) ^ p
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ (1 / p) ≤ a + b

Tactic:
lift a to NNReal using ha

Goal state after:
p b : ℝ
hb : 0 ≤ b
hp1 : 1 ≤ p
a : ℝ≥0
⊢ (↑a ^ p + b ^ p) ^ (1 / p) ≤ ↑a + b
Module: Mathlib.Analysis.MeanInequalitiesPow

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

Tactic:
lift a to NNReal using ha

Goal state after:
p q b : ℝ
hb : 0 ≤ b
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0
⊢ (↑a ^ q + b ^ q) ^ (1 / q) ≤ (↑a ^ p + b ^ p) ^ (1 / p)
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hp : 0 ≤ p
hp1 : p ≤ 1
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
lift a to NNReal using ha

Goal state after:
p b : ℝ
hb : 0 ≤ b
hp : 0 ≤ p
hp1 : p ≤ 1
a : ℝ≥0
⊢ (↑a + b) ^ p ≤ ↑a ^ p + b ^ p
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

Tactic:
rcases hp.eq_or_lt with rfl | hp
  · rw [zero_add] at hpq
    simp [hpq]
  rcases hq.eq_or_lt with rfl | hq
  · rw [add_zero] at hpq
    simp [hpq]
  have h2p : 1 < 1 / p := by
    rw [one_div, one_lt_inv₀ hp]
    linarith
  have h2pq : (1 / p)⁻¹ + (1 / q)⁻¹ = 1 := by simp [hpq]
  have := ENNReal.lintegral_mul_le_Lp_mul_Lq μ (Real.holderConjugate_iff.mpr ⟨h2p, h2pq⟩)
    (hf.pow_const p) (hg.pow_const q)
  simpa [← ENNReal.rpow_mul, hp.ne', hq.ne'] using this

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

Goal state before:
pp: case insert.inl
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : ∑ i ∈ insert i₀ s, p i = 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
⊢ ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ ≤
    (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i

Tactic:
have h2p : ∀ i ∈ s, p i = 0 := by
        simpa [hi₀, h2i₀, sum_eq_zero_iff_of_nonneg (fun i hi ↦ h2p i <| mem_insert_of_mem hi)]
          using hp

Goal state after:
case insert.inl
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : ∑ i ∈ insert i₀ s, p i = 1
h2p✝ : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
h2p : ∀ i ∈ s, p i = 0
⊢ ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ ≤
    (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
s : Set α
hfq : MemLp f q (μ.restrict (toMeasurable μ s))
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ∞
hpq : p ≤ q
this : (toMeasurable μ s).indicator f = f
⊢ MemLp f p (μ.restrict (toMeasurable μ s))

Tactic:
have : Fact (μ (toMeasurable μ s) < ∞) := ⟨by simpa [lt_top_iff_ne_top] using hs⟩

Goal state after:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
s : Set α
hfq : MemLp f q (μ.restrict (toMeasurable μ s))
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ∞
hpq : p ≤ q
this✝ : (toMeasurable μ s).indicator f = f
this : Fact (μ (toMeasurable μ s) < ∞)
⊢ MemLp f p (μ.restrict (toMeasurable μ s))
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr.calc_1
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ ∑ i ∈ s, w i * f i = ∑ i ∈ s, w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i)

pp: case inr.calc_2
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ (∑ i ∈ s, (w i ^ (1 - p⁻¹)) ^ (1 - p⁻¹)⁻¹) ^ (1 / (1 - p⁻¹)⁻¹) * (∑ i ∈ s, (w i ^ p⁻¹ * f i) ^ p) ^ (1 / p) =
    (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

Tactic:
· congr with i
    rw [← mul_assoc, ← rpow_of_add_eq _ one_ne_zero, rpow_one]
    simp

Goal state after:
case inr.calc_2
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ (∑ i ∈ s, (w i ^ (1 - p⁻¹)) ^ (1 - p⁻¹)⁻¹) ^ (1 / (1 - p⁻¹)⁻¹) * (∑ i ∈ s, (w i ^ p⁻¹ * f i) ^ p) ^ (1 / p) =
    (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x✝ : MeasurableSpace α
inst✝ : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ i ∈ ∅, MemLp (f i) (p i) μ
hμ : μ = 0
⊢ MemLp (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ

Tactic:
simp [MemLp, eLpNormEssSup_const, hμ, aestronglyMeasurable_const, Pi.one_def]

Goal state after: