mathlib-initiative/mathlib-tactics huggingface dataset:
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
h_eq : ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)
⊢ ∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k

Tactic:
by_contra!; exact h_eq.not_gt <| hf.map_sum_lt h₀ h₁ hmem this

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 : 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, p j = ∑ i ∈ t, w i • p i

Tactic:
refine ⟨?_, fun h ↦ ?_⟩
  · obtain rfl | ⟨i₀, hi₀⟩ := t.eq_empty_or_nonempty
    · simp
    intro h_eq i hi
    have H (j) (hj : j ∈ t) : p j = p i₀ := hf.eq_of_le_map_sum h₀ h₁ hmem h_eq.ge hj hi₀
    calc p i = p i₀ := by rw [H _ hi]
      _ = (1 : 𝕜) • p i₀ := by simp
      _ = (∑ j ∈ t, w j) • p i₀ := by rw [h₁]
      _ = ∑ j ∈ t, (w j • p i₀) := by rw [sum_smul]
      _ = ∑ j ∈ t, (w j • p j) := by congr! 2 with j hj; rw [← H _ hj]
  · grind [hf.map_sum_eq_iff_of_pos h₀ h₁ hmem]

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

Goal state before:
pp: case refine_1.refine_2
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ id ((p i).ball 0 ε) ⊆ ⇑(p i) ⁻¹' Metric.ball 0 ε

Tactic:
id,

Goal state after:
case refine_1.refine_2
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ (p i).ball 0 ε ⊆ ⇑(p i) ⁻¹' Metric.ball 0 ε
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_2
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
s : Finset ι
r : ℝ
hr : 0 < r
hU : (s.sup p).ball 0 r ∈ p.basisSets
⊢ id ((s.sup p).ball 0 r) ∈ ⨅ i, comap (⇑(p i)) (𝓝 0)

Tactic:
id,

Goal state after:
case refine_2
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
s : Finset ι
r : ℝ
hr : 0 < r
hU : (s.sup p).ball 0 r ∈ p.basisSets
⊢ (s.sup p).ball 0 r ∈ ⨅ i, comap (⇑(p i)) (𝓝 0)
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case mpr
𝕜 : 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
h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
s' : Set E
hs'✝ : s' ∈ p.basisSets
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = (I.sup p).ball 0 r
⊢ Absorbs 𝕜 (id s') s

Tactic:
id,

Goal state after:
case mpr
𝕜 : 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
h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
s' : Set E
hs'✝ : s' ∈ p.basisSets
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = (I.sup p).ball 0 r
⊢ Absorbs 𝕜 s' s
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✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
⊢ CompleteSpace (E →SLᵤ[σ, 𝔖] F)

Tactic:
wlog hF : T2Space F generalizing F
  · rw [(isUniformInducing_postcomp σ (SeparationQuotient.mkCLM 𝕜₂ F)
      SeparationQuotient.isUniformInducing_mk _).completeSpace_congr]
    exacts [this _ inferInstance, SeparationQuotient.postcomp_mkCLM_surjective F σ E]
  rw [completeSpace_iff_isComplete_range (isUniformInducing_coeFn _ _ _)]
  apply IsClosed.isComplete
  have H₁ : IsClosed {f : E →ᵤ[𝔖] F | Continuous ((UniformOnFun.toFun 𝔖) f)} :=
    UniformOnFun.isClosed_setOfPred_continuous h𝔖
  convert!
    H₁.inter <|
      (LinearMap.isClosed_range_coe E F σ).preimage
        (UniformOnFun.uniformContinuous_toFun h𝔖U).continuous
  exact ContinuousLinearMap.range_coeFn_eq

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
𝕜' : Type u_9
inst✝³ : DistribSMul 𝕜' F
inst✝² : SMulCommClass 𝕜₂ 𝕜' F
inst✝¹ : SeminormedAddCommGroup 𝕜'
inst✝ : IsBoundedSMul 𝕜' F
c : 𝕜'
f : E →SL[σ₁₂] F
x✝ : E
⊢ ‖(c • f) x✝‖ ≤ ‖c‖ * ‖f‖ * ‖x✝‖

Tactic:
smul_apply,

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
𝕜' : Type u_9
inst✝³ : DistribSMul 𝕜' F
inst✝² : SMulCommClass 𝕜₂ 𝕜' F
inst✝¹ : SeminormedAddCommGroup 𝕜'
inst✝ : IsBoundedSMul 𝕜' F
c : 𝕜'
f : E →SL[σ₁₂] F
x✝ : E
⊢ ‖c • f x✝‖ ≤ ‖c‖ * ‖f‖ * ‖x✝‖
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜₂ F
𝕜₁ : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup G
𝕜₃ : Type u_7
inst✝⁸ : NormedField 𝕜₃
inst✝⁷ : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst✝⁶ : RingHomSurjective τ
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousConstSMul 𝕜₂ F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] E →SLᵤ[σ, 𝔖] F
hB : Continuous[instTopologicalSpaceProd, inst✝⁵] fun p ↦ (B p.1) p.2
S : Set E
hS : S ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
V : Set G
hV : V ∈ 𝓝 0
W : Set E
hW : W ∈ 𝓝 0
hVW : V ×ˢ W ⊆ (fun p ↦ (B p.1) p.2) ⁻¹' U
c : 𝕜₁
hc : MapsTo (fun x ↦ c • x) S W
c_ne : c ≠ 0
d : 𝕜₃
hd : τ d = σ c
d_ne : d ≠ 0
a : G
ha : a ∈ V
x : E
hx : x ∈ S
⊢ (σ c • B a) x ∈ U

Tactic:
smul_apply,

Goal state after:
𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜₂ F
𝕜₁ : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup G
𝕜₃ : Type u_7
inst✝⁸ : NormedField 𝕜₃
inst✝⁷ : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst✝⁶ : RingHomSurjective τ
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousConstSMul 𝕜₂ F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] E →SLᵤ[σ, 𝔖] F
hB : Continuous[instTopologicalSpaceProd, inst✝⁵] fun p ↦ (B p.1) p.2
S : Set E
hS : S ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
V : Set G
hV : V ∈ 𝓝 0
W : Set E
hW : W ∈ 𝓝 0
hVW : V ×ˢ W ⊆ (fun p ↦ (B p.1) p.2) ⁻¹' U
c : 𝕜₁
hc : MapsTo (fun x ↦ c • x) S W
c_ne : c ≠ 0
d : 𝕜₃
hd : τ d = σ c
d_ne : d ≠ 0
a : G
ha : a ∈ V
x : E
hx : x ∈ S
⊢ σ c • (B a) x ∈ U
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case neg
𝕜 : Type u_2
F : Type u_7
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑q
hq' : Tendsto (⇑q) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : {y | ‖y‖ < ε} ⊆ ⇑q ⁻¹' Iio 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < ‖c‖ / ε
x✝ : F
hx : ¬‖x✝‖ = 0
x : F
hle : ε / ‖c‖ ≤ (normSeminorm 𝕜 F) x
hlt : (normSeminorm 𝕜 F) x < ε
⊢ 1 / (‖c‖ / ε) ≤ (normSeminorm 𝕜 F) x

Tactic:
one_div_div

Goal state after:
case neg
𝕜 : Type u_2
F : Type u_7
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑q
hq' : Tendsto (⇑q) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : {y | ‖y‖ < ε} ⊆ ⇑q ⁻¹' Iio 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < ‖c‖ / ε
x✝ : F
hx : ¬‖x✝‖ = 0
x : F
hle : ε / ‖c‖ ≤ (normSeminorm 𝕜 F) x
hlt : (normSeminorm 𝕜 F) x < ε
⊢ ε / ‖c‖ ≤ (normSeminorm 𝕜 F) x
Module: Mathlib.Analysis.Normed.Operator.NNNorm

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

Tactic:
calc
    r < 1⁻¹ * ‖f x‖₊ := by simpa
    _ < ‖x‖₊⁻¹ * ‖f x‖₊ := by gcongr; exact hr.pos

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : 𝐤X → Y
⊢ Continuous[instTopologicalSpace, inst✝] f ↔
    ∀ (K : Set X), IsCompact K → ContinuousOn (f ∘ ⇑(CompactCoherentification.mk X)) K

Tactic:
by
  simp_rw [continuous_coinduced_dom, continuous_iSup_dom, continuous_coinduced_dom,
    continuousOn_iff_continuous_domRestrict]
  rfl

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup F
inst✝⁸ : SeminormedAddCommGroup G
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NontriviallyNormedField 𝕜₃
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x : E
y : F
⊢ ‖(f x) y‖ ≤ ‖f.flip‖ * ‖x‖ * ‖y‖

Tactic:
rw [mul_right_comm]

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup F
inst✝⁸ : SeminormedAddCommGroup G
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NontriviallyNormedField 𝕜₃
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x : E
y : F
⊢ ‖(f x) y‖ ≤ ‖f.flip‖ * ‖y‖ * ‖x‖
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]

Goal state after:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inst✝ : f.NeBot
⊢ (∃ b, ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, ↑(u a_1) ≤ a) → b ≤ a) ↔
    ∃ x,
      ∃ (hx : 0 ≤ x),
        ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
          (∀ᶠ (a : ι) in f, ↑(u a) ≤ ↑(NNReal.mk x_1 hx_1)) → ↑(NNReal.mk x hx) ≤ ↑(NNReal.mk x_1 hx_1)
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
⊢ (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]

Goal state after:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
⊢ (∃ b, ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, ↑(u a_1) ≥ a) → b ≥ a) ↔
    ∃ x,
      ∃ (hx : 0 ≤ x),
        ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
          (∀ᶠ (a : ι) in f, ↑(NNReal.mk x_1 hx_1) ≤ ↑(u a)) → ↑(NNReal.mk x_1 hx_1) ≤ ↑(NNReal.mk x hx)
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : 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
⊢ ENNReal.ofReal (u a) < some x

Tactic:
obtain ha₀ | ha₀ := le_total (u a) 0

Goal state after:
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

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.MeasureTheory.Function.AEEqFun

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ∃ b, f = mk (const α b) ⋯
⊢ mk (const α (Classical.choose h)) ⋯ = f

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ b, f = mk (const α b) ⋯
⊢ mk (AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯) ⋯ = f

Tactic:
· exact Classical.choose_spec h |>.symm

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ b, f = mk (const α b) ⋯
⊢ mk (AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯) ⋯ = f
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₂ = mk (fun a ↦ g (↑f₁ a) (↑f₂ a)) ⋯

Tactic:
comp₂_eq_pair,

Goal state after:
α : 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 (uncurry g) hg (f₁.pair f₂) = mk (fun a ↦ g (↑f₁ a) (↑f₂ a)) ⋯
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : ConditionallyCompleteLattice β
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
f : α → β
⊢ essSup f (c • μ) = essSup f μ

Tactic:
essSup,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : ConditionallyCompleteLattice β
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
f : α → β
⊢ limsup f (ae (c • μ)) = limsup f (ae μ)
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : ConditionallyCompleteLattice β
c : ℝ≥0∞
hc : c ≠ 0
f : α → β
⊢ essSup f (c • μ) = essSup f μ

Tactic:
essSup,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : ConditionallyCompleteLattice β
c : ℝ≥0∞
hc : c ≠ 0
f : α → β
⊢ limsup f (ae (c • μ)) = limsup f (ae μ)
Module: Mathlib.MeasureTheory.Function.EssSup

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

Tactic:
essSup,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : ConditionallyCompleteLattice β
f : α → β
inst✝ : Nonempty α
hμ : ∀ (a : α), μ {a} ≠ 0
hf : BddAbove (range f)
⊢ limsup f (ae μ) = ⨆ a, f a
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:
essSup,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
hμ : ∀ (a : α), μ {a} ≠ 0
f : α → β
⊢ limsup f (ae μ) = ⨆ i, f i
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
X : δ → Type u_5
inst✝¹ : (i : δ) → MeasurableSpace (X i)
l : List δ
μ : (i : δ) → Measure (X i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
⊢ SigmaFinite (Measure.tprod l μ)

Tactic:
induction l with
  | nil => rw [tprod_nil]; infer_instance
  | cons i l ih => rw [tprod_cons]; exact @prod.instSigmaFinite _ _ _ _ _ _ _ ih

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✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
⊢ eLpNorm (s.indicator f) p μ ≤ eLpNorm f p μ

Tactic:
apply eLpNorm_mono_enorm
  simp_rw [enorm_indicator_eq_indicator_enorm]
  exact s.indicator_le_self _

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
α : ι✝ → Type u_3
inst✝⁷ : Fintype ι✝
m : (i : ι✝) → OuterMeasure (α i)
inst✝⁶ : (i : ι✝) → MeasurableSpace (α i)
μ✝ : (i : ι✝) → Measure (α i)
inst✝⁵ : ∀ (i : ι✝), SigmaFinite (μ✝ i)
ι : Type u_4
inst✝⁴ : Fintype ι
X : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (X i)
inst✝² : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : ∀ (i : ι), IsUnifLocDoublingMeasure (μ i)
⊢ IsUnifLocDoublingMeasure (Measure.pi μ)

Tactic:
use ∏ i, IsUnifLocDoublingMeasure.doublingConstant (μ i)

Goal state after:
case h
ι✝ : Type u_1
ι' : Type u_2
α : ι✝ → Type u_3
inst✝⁷ : Fintype ι✝
m : (i : ι✝) → OuterMeasure (α i)
inst✝⁶ : (i : ι✝) → MeasurableSpace (α i)
μ✝ : (i : ι✝) → Measure (α i)
inst✝⁵ : ∀ (i : ι✝), SigmaFinite (μ✝ i)
ι : Type u_4
inst✝⁴ : Fintype ι
X : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (X i)
inst✝² : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : ∀ (i : ι), IsUnifLocDoublingMeasure (μ i)
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : (i : ι) → X i),
      (Measure.pi μ) (Metric.closedBall x (2 * ε)) ≤
        ↑(∏ i, IsUnifLocDoublingMeasure.doublingConstant (μ i)) * (Measure.pi μ) (Metric.closedBall x ε)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableInv (α i)
inst✝ : ∀ (i : ι), (μ i).IsInvInvariant
⊢ (Measure.pi μ).IsInvInvariant

Tactic:
refine ⟨(Measure.pi_eq fun s hs => ?_).symm⟩
  have A : Inv.inv ⁻¹' pi univ s = Set.pi univ fun i => Inv.inv ⁻¹' s i := by ext; simp
  simp_rw [Measure.inv, Measure.map_apply measurable_inv (MeasurableSet.univ_pi hs), A, pi_pi,
    measure_preimage_inv]

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

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
this : ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun x ↦ c) x‖
⊢ eLpNorm (s.indicator (f - g)) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)

Tactic:
grw [eLpNorm_mono this, eLpNorm_indicator_const hs hp hp', ← ofReal_norm,
    Real.norm_eq_abs, abs_of_nonneg hc]

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

Goal state before:
pp: case refine_1
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
⊢ Prod.instMeasurableSpace =
    generateFrom
      (image2 (fun x1 x2 ↦ x1 ×ˢ x2) (univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s})
        (univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}))

Tactic:
refine (generateFrom_eq_prod generateFrom_pi generateFrom_pi ?_ ?_).symm
      · exact (FiniteSpanningSetsIn.pi (fun i ↦ (μ i).toFiniteSpanningSetsIn)).isCountablySpanning
      · exact (FiniteSpanningSetsIn.pi (fun i ↦ (ν i).toFiniteSpanningSetsIn)).isCountablySpanning

Goal state after:
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:
by
  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
F : Type u_5
G : Type u_6
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → 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 [enorm, hx]

Goal state after:
α : Type u_1
F : Type u_5
G : Type u_6
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊
this : (fun x ↦ ‖f x‖ₑ ^ q) =ᵐ[μ] fun x ↦ ‖g x‖ₑ ^ q
⊢ eLpNorm' f q μ = eLpNorm' g q μ
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: case inl
p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
⊢ 0⁻¹ - q⁻¹ = p⁻¹

Tactic:
suffices p = 0 by simpa [this]
    by_contra! hp
    have := calc
      0⁻¹ = p⁻¹ + q⁻¹ := inv_eq p q 0
      _ < ⊤ + ⊤ := by simp [hp, hq, pos_iff_ne_zero]
      _ = ⊤ := by simp
    simp_all

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

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

Tactic:
rcases lt_or_gt_of_ne hya with hya | hya
    · convert! hf.secant_strict_mono_aux3 hx ha hxy hya using 1 <;> rw [← neg_div_neg_eq] <;>
        simp
    · convert! hf.slope_strict_mono_adjacent hx hy hxa hya using 1
      rw [← neg_div_neg_eq]; simp

Goal state after: