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

Goal state before:
pp: case inl
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
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ ∃ t ⊆ pathComponentIn u (inl x), IsOpen[instTopologicalSpaceSum] t ∧ inl x ∈ t

pp: case inr
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
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ ∃ t ⊆ pathComponentIn u (inr y), IsOpen[instTopologicalSpaceSum] t ∧ inr y ∈ t

Tactic:
· refine ⟨Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x, ?_, ?_, ?_⟩
    · apply IsPathConnected.subset_pathComponentIn
      · exact (isPathConnected_pathComponentIn (by exact hxu)).image continuous_inl
      · exact ⟨x, mem_pathComponentIn_self hxu, rfl⟩
      · exact (image_mono pathComponentIn_subset).trans (u.image_preimage_subset _)
    · exact isOpenMap_inl _ <| (hu.preimage continuous_inl).pathComponentIn _
    · exact ⟨x, mem_pathComponentIn_self hxu, rfl⟩

Goal state after:
case inr
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
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ ∃ t ⊆ pathComponentIn u (inr y), IsOpen[instTopologicalSpaceSum] t ∧ inr y ∈ t
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
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:
· exact isOpenMap_sigmaMk _ <| (hu.preimage continuous_sigmaMk).pathComponentIn _

Goal state after:
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.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
x : F
h : x ∈ closedBall 0 r
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
x✝ : Invertible 2
z : F
hz : z ∈ sphere ?m.155 r
⊢ midpoint ℝ z (-z) ∈ U

Tactic:
exact Convex.midpoint_mem hU (hU_sub hz) <| hU_sub (by simp_all)

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
ι : Type u_8
b : AffineBasis ι R E
⊢ (convexHull R) (Set.range ⇑b) = {x | ∀ (i : ι), 0 ≤ (b.coord i) x}

Tactic:
rw [convexHull_range_eq_exists_affineCombination]
  ext x
  refine ⟨?_, fun hx => ?_⟩
  · rintro ⟨s, w, hw₀, hw₁, rfl⟩ i
    by_cases hi : i ∈ s
    · rw [b.coord_apply_combination_of_mem hi hw₁]
      exact hw₀ i hi
    · rw [b.coord_apply_combination_of_notMem hi hw₁]
  · have hx' : x ∈ affineSpan R (range b) := by
      rw [b.tot]
      exact AffineSubspace.mem_top R E x
    obtain ⟨s, w, hw₁, rfl⟩ := (mem_affineSpan_iff_eq_affineCombination R E).mp hx'
    refine ⟨s, w, ?_, hw₁, rfl⟩
    intro i hi
    specialize hx i
    rw [b.coord_apply_combination_of_mem hi hw₁] at hx
    exact hx

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
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜₂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : T2Space F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = univ
⊢ T2Space (E →SLᵤ[σ, 𝔖] F)

Tactic:
by
  let : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
  have : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  have : T2Space (E →ᵤ[𝔖] F) := UniformOnFun.t2Space_of_covering h𝔖
  exact (isEmbedding_coeFn σ F 𝔖).t2Space

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
inst✝⁷ : AddCommGroup G
inst✝⁶ : UniformSpace G
inst✝⁵ : IsUniformAddGroup G
𝕜₃ : Type u_6
inst✝⁴ : NormedField 𝕜₃
inst✝³ : Module 𝕜₃ G
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝² : RingHomCompTriple σ τ ρ
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
g : F →SL[τ] G
hg : IsUniformInducing ⇑g
𝔖 : Set (Set E)
⊢ IsUniformInducing g.comp

Tactic:
rw [← (isUniformInducing_coeFn _ _ _).of_comp_iff]

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✝⁷ : AddCommGroup G
inst✝⁶ : UniformSpace G
inst✝⁵ : IsUniformAddGroup G
𝕜₃ : Type u_6
inst✝⁴ : NormedField 𝕜₃
inst✝³ : Module 𝕜₃ G
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝² : RingHomCompTriple σ τ ρ
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
g : F →SL[τ] G
hg : IsUniformInducing ⇑g
𝔖 : Set (Set E)
⊢ IsUniformInducing ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) ∘ g.comp)
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).filter
t : Set E
ht : t ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).toFilterBasis
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = (w.sup fun x ↦ p).ball 0 r
w_ne : w ≠ ∅
this : t = p.ball 0 r
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < r
c_ne : c ≠ 0
⊢ c • p.ball 0 1 ⊆ p.ball 0 r

Tactic:
rw [smul_ball_zero c_ne]

Goal state after:
𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).filter
t : Set E
ht : t ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).toFilterBasis
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = (w.sup fun x ↦ p).ball 0 r
w_ne : w ≠ ∅
this : t = p.ball 0 r
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < r
c_ne : c ≠ 0
⊢ p.ball 0 (‖c‖ * 1) ⊆ p.ball 0 r
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: case inr
𝕜 : 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 σ₁₂
f : E →SL[σ₁₂] F
M : ℝ≥0
hM : ∀ (x : E), ‖f x‖ₑ ≤ ↑M * ‖x‖ₑ
h'M : ↑M < ∞
⊢ ‖f‖ₑ ≤ ↑M

Tactic:
simp only [← ofReal_norm, ENNReal.ofReal_le_coe]

Goal state after:
case inr
𝕜 : 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 σ₁₂
f : E →SL[σ₁₂] F
M : ℝ≥0
hM : ∀ (x : E), ‖f x‖ₑ ≤ ↑M * ‖x‖ₑ
h'M : ↑M < ∞
⊢ ‖f‖ ≤ ↑M
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case mpr.inl
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb₀ : 0 ≤ b
hb : ∀ (x : ℝ) (hx : 0 ≤ x), (∀ᶠ (a : ι) in f, ↑(NNReal.mk x hx) ≤ ↑(u a)) → ↑(NNReal.mk x hx) ≤ ↑(NNReal.mk b hb₀)
x : ℝ
hx : ∀ᶠ (a : ι) in f, ↑(u a) ≥ x
hx₀ : x ≤ 0
⊢ b ≥ x

pp: case mpr.inr
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb₀ : 0 ≤ b
hb : ∀ (x : ℝ) (hx : 0 ≤ x), (∀ᶠ (a : ι) in f, ↑(NNReal.mk x hx) ≤ ↑(u a)) → ↑(NNReal.mk x hx) ≤ ↑(NNReal.mk b hb₀)
x : ℝ
hx : ∀ᶠ (a : ι) in f, ↑(u a) ≥ x
hx₀ : 0 ≤ x
⊢ b ≥ x

Tactic:
· exact hx₀.trans hb₀

Goal state after:
case mpr.inr
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb₀ : 0 ≤ b
hb : ∀ (x : ℝ) (hx : 0 ≤ x), (∀ᶠ (a : ι) in f, ↑(NNReal.mk x hx) ≤ ↑(u a)) → ↑(NNReal.mk x hx) ≤ ↑(NNReal.mk b hb₀)
x : ℝ
hx : ∀ᶠ (a : ι) in f, ↑(u a) ≥ x
hx₀ : 0 ≤ x
⊢ b ≥ x
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

Goal state after:
Ω : 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
this : ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E
⊢ ∑ x, μ (X ⁻¹' {x} ∩ E) = μ E
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
⊢ x✝ ∈ univ.pi (update (fun i' ↦ iUnion (t i')) i (⋃ x, s)) ↔ x✝ ∈ univ.pi fun k ↦ ⋃ j, update (fun i' ↦ t i' j) i s k

Tactic:
simp_rw [mem_univ_pi]

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
⊢ (∀ (i_1 : ι), x✝ i_1 ∈ update (fun i' ↦ iUnion (t i')) i (⋃ x, s) i_1) ↔
    ∀ (i_1 : ι), x✝ i_1 ∈ ⋃ j, update (fun i' ↦ t i' j) i s i_1
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
hμ : ∀ (a : α), μ {a} ≠ 0
f : α → β
⊢ essSup f μ = ⨆ i, f i

Tactic:
rw [essSup, ae_eq_top.2 hμ, limsup_top_eq_iSup]

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

Goal state before:
pp: x y z : ℝ
⊢ x ∈ Ioi 0 → z ∈ Ioi 0 → x < y → y < z → (log z - log y) / (z - y) < (log y - log x) / (y - x)

Tactic:
(hx : 0 < x)

Goal state after:
x y z : ℝ
hx : 0 < x
⊢ z ∈ Ioi 0 → x < y → y < z → (log z - log y) / (z - y) < (log y - log x) / (y - x)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
⊢ eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹

Tactic:
by
  simpa [C.enorm_eq, ENNReal.smul_def, smul_eq_mul] using
    (eLpNorm_le_of_ae_enorm_bound (f := f) (C := (C : ℝ≥0∞))
      (hfC.mono fun _ hx => by simpa using hx))

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

Goal state before:
pp: case inr.inr.inr
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ 1 + s < 1 + p * s

Tactic:
· gcongr
      exact lt_mul_of_one_lt_left hs' hp

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

Goal state before:
pp: p : ℝ≥0
hp : 1 < p
⊢ p = p - 1 + 1

Tactic:
tsub_add_cancel_of_le hp.le

Goal state after:
p : ℝ≥0
hp : 1 < p
⊢ p = p
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

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

Tactic:
grw [h, eLpNorm_smul_measure_le]

Goal state after:
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
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
key : ((-f) x - (-f) a) / (x - a) < ((-f) y - (-f) a) / (y - a)
⊢ (f y - f a) / (y - a) < (f x - f a) / (x - a)

Tactic:
simp only [Pi.neg_apply] at key

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
key : (-f x - -f a) / (x - a) < (-f y - -f a) / (y - a)
⊢ (f y - f a) / (y - a) < (f x - f a) / (x - a)
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConcaveOn 𝕜 s f
x y : 𝕜
hy : y ∈ s
hxy : x < y
hxy' : f x < f y
⊢ StrictMonoOn f (s ∩ Set.Iic x)

Tactic:
by
  simpa using (neg_convexOn_iff.mpr hf |>.strictAntiOn hy hxy <| neg_lt_neg hxy').neg

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
⊢ (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)

Tactic:
rcases eq_or_lt_of_le hp with (rfl | h'p)
  · simp only [rpow_one, sub_self, rpow_zero, one_mul]; rfl
  convert!
    rpow_arith_mean_le_arith_mean2_rpow (1 / 2) (1 / 2) (2 * z₁) (2 * z₂) (add_halves 1) hp using 1
  · simp only [one_div, inv_mul_cancel_left₀, Ne, two_ne_zero,
      not_false_iff]
  · have A : p - 1 ≠ 0 := ne_of_gt (sub_pos.2 h'p)
    simp only [mul_rpow, rpow_sub' A, rpow_one]
    ring

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: z₁ z₂ p : ℝ≥0∞
⊢ (z₁ + z₂) ^ p.toReal⁻¹ ≤ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)

Tactic:
by_cases p_zero : p = 0
  · simp [p_zero, LpAddConst_zero]
  convert rpow_add_le_mul_rpow_add_rpow' z₁ z₂ (p := p.toReal⁻¹) (by positivity)
  rw [← ENNReal.toReal_inv, ENNReal.ofReal_toReal (by simpa), inv_inv]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Tactic:
by
  have h0_rpow : (∫⁻ a, (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0 := by
    simp [h_add_zero, h_add_top, -Pi.add_apply]
  suffices h :
    1 ≤
      (∫⁻ a : α, (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
        ((∫⁻ a : α, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a : α, g a ^ p ∂μ) ^ (1 / p)) by
    rwa [← ENNReal.mul_le_mul_iff_right h0_rpow (by finiteness),
      ← mul_assoc, ← rpow_add _ _ h_add_zero h_add_top, ←
      sub_eq_add_neg, _root_.sub_self, rpow_zero, one_mul, mul_one] at h
  have h :
    (∫⁻ a : α, (f + g) a ^ p ∂μ) ≤
      ((∫⁻ a : α, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a : α, g a ^ p ∂μ) ^ (1 / p)) *
        (∫⁻ a : α, (f + g) a ^ p ∂μ) ^ (1 / q) :=
    lintegral_rpow_add_le_add_eLpNorm_mul_lintegral_rpow_add hpq hf hg
  have h_one_div_q : 1 / q = 1 - 1 / p := by
    nth_rw 2 [← hpq.inv_add_inv_eq_one]
    ring
  simp_rw [h_one_div_q, sub_eq_add_neg 1 (1 / p), ENNReal.rpow_add _ _ h_add_zero h_add_top,
    rpow_one] at h
  conv_rhs at h => enter [2]; rw [mul_comm]
  conv_lhs at h => rw [← one_mul (∫⁻ a : α, (f + g) a ^ p ∂μ)]
  rwa [← mul_assoc, ENNReal.mul_le_mul_iff_left h_add_zero h_add_top, mul_comm] at h

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this : (∑ i ∈ s, (|f i| + |g i|) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)
⊢ (∑ i ∈ s, |f i + g i| ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)

Tactic:
refine le_trans (rpow_le_rpow ?_ (sum_le_sum fun i _ => ?_) ?_) this

Goal state after:
case refine_1
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this : (∑ i ∈ s, (|f i| + |g i|) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)
⊢ 0 ≤ ∑ i ∈ s, |f i + g i| ^ p

case refine_2
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this : (∑ i ∈ s, (|f i| + |g i|) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)
i : ι
x✝ : i ∈ s
⊢ |f i + g i| ^ p ≤ (|f i| + |g i|) ^ p

case refine_3
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this : (∑ i ∈ s, (|f i| + |g i|) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)
⊢ 0 ≤ 1 / p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3.a
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ f i * g i = |f i * g i|

Tactic:
rw [abs_of_nonneg (mul_nonneg (hf i hi) (hg i hi))]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: case e_a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ = ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ

Tactic:
simp_rw [← ofReal_norm]

Goal state after:
case e_a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ ENNReal.ofReal ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ =
    ∑ x ∈ Finset.range (n + 1), ENNReal.ofReal ‖f (x + 1) a - f x a‖
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop
⊢ ∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p

Tactic:
h_tsum_1 _

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop
⊢ ∫⁻ (a : α), liminf (fun n ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop ^ p ∂μ ≤
    liminf (fun n ↦ ∑ i ∈ Finset.range (n + 1), B i) atTop ^ p
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f : ↥(Lp E p μ)
⊢ ‖hg.compLp g0 f‖ ≤ ↑c * ‖f‖

Tactic:
simpa only [compLp_zero, sub_zero] using hg.norm_compLp_sub_le g0 f 0

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
hp : 1 ≤ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) ∞ μ < B N
hp_top : True
⊢ ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N

Tactic:
ae_all_iff

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
hp : 1 ≤ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) ∞ μ < B N
hp_top : True
⊢ ∀ (i i_1 i_2 : ℕ), i ≤ i_1 → i ≤ i_2 → ∀ᵐ (a : α) ∂μ, ‖(f i_1 - f i_2) a‖ₑ < B i
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: case pos.refine_1
α : Type u_1
m✝ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
hp : 1 ≤ ∞
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x ↦ ‖(f n - f m) x‖ₑ) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
n m N : ℕ
⊢ N ≤ n → N ≤ m → dist (f n x) (f m x) ≤ (B N).toReal

Tactic:
hnN

Goal state after:
case pos.refine_1
α : Type u_1
m✝ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
hp : 1 ≤ ∞
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x ↦ ‖(f n - f m) x‖ₑ) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
n m N : ℕ
hnN : N ≤ n
⊢ N ≤ m → dist (f n x) (f m x) ≤ (B N).toReal
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
⊢ Disjoint (Set.range ⇑(inl.trans f, inr.trans f).1) (Set.range ⇑(inl.trans f, inr.trans f).2)

Tactic:
rw [Set.disjoint_left]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
⊢ ∀ ⦃a : γ⦄, a ∈ Set.range ⇑(inl.trans f, inr.trans f).1 → ¬a ∈ Set.range ⇑(inl.trans f, inr.trans f).2