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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConcaveOn ℝ C f
this :
  [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) |f|].TFAE
⊢ [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (𝓝 x₀) f,
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (𝓝 x₀) f,
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) |f|].TFAE

Tactic:
convert! this using 8 <;> exact (Equiv.neg ℝ).exists_congr (by simp)

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

Goal state before:
pp: f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
this : ContinuousOn f (Ico y z) ∧ ContinuousOn f (Ioc y z)
⊢ ContinuousOn f (Icc y z)

Tactic:
intro x hx
    rcases eq_or_lt_of_le (α := ℝ) hx.1 with rfl | hyx
    · exact hfy.mono (by grind)
    rcases eq_or_lt_of_le (α := ℝ) hx.2 with rfl | hxz
    · exact hfz.mono (by grind)
    have hx := this.1 x (by grind)
    rw [continuousWithinAt_iff_continuousAt (Ico_mem_nhds hyx hxz)] at hx
    exact hx.continuousWithinAt

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Prod

Goal state before:
pp: I : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
X : Type u_3
Y : Type u_4
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
⊢ ∀ (f : StdSimplex R (StdSimplex R (X × Y))),
    (iConvexComb (StdSimplex.map (fun w ↦ (iConvexComb w fst, iConvexComb w snd)) f) fst,
        iConvexComb (StdSimplex.map (fun w ↦ (iConvexComb w fst, iConvexComb w snd)) f) snd) =
      (iConvexComb (sConvexComb f) fst, iConvexComb (sConvexComb f) snd)

Tactic:
simp [iConvexComb_assoc]

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Prod

Goal state before:
pp: I : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
ι : Type u_3
X : ι → Type u_4
inst✝ : (i : ι) → ConvexSpace R (X i)
i : ι
⊢ ∀ (f : StdSimplex R (StdSimplex R ((i : ι) → X i))),
    (fun i ↦ iConvexComb (StdSimplex.map (fun w i ↦ iConvexComb w fun x ↦ x i) f) fun x ↦ x i) = fun i ↦
      iConvexComb (sConvexComb f) fun x ↦ x i

Tactic:
simp [iConvexComb_assoc]

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Prod

Goal state before:
pp: I : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst✝¹ : Zero X
inst✝ : ConvexSpace R X
i : ι
w : StdSimplex R (StdSimplex R (ι →₀ X))
a✝ : ι
⊢ (onFinset
        ((StdSimplex.map (fun w ↦ onFinset (w.weights.support.biUnion support) (fun i ↦ iConvexComb w fun x ↦ x i) ⋯)
                  w).weights.support.biUnion
          support)
        (fun i ↦
          iConvexComb
            (StdSimplex.map (fun w ↦ onFinset (w.weights.support.biUnion support) (fun i ↦ iConvexComb w fun x ↦ x i) ⋯)
              w)
            fun x ↦ x i)
        ⋯)
      a✝ =
    (onFinset ((sConvexComb w).weights.support.biUnion support) (fun i ↦ iConvexComb (sConvexComb w) fun x ↦ x i) ⋯) a✝

Tactic:
simp [iConvexComb_assoc]

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: ι : Type u_1
I : Type u_2
R : Type u_3
K : Type u_4
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
w✝ : StdSimplex R X
s✝ t : Set X
x y : X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R (StdSimplex R ↑s)
⊢ ↑⟨iConvexComb (StdSimplex.map (fun w ↦ ⟨iConvexComb w Subtype.val, ⋯⟩) w) Subtype.val, ⋯⟩ =
    ↑⟨iConvexComb (sConvexComb w) Subtype.val, ⋯⟩

Tactic:
simp [iConvexComb_assoc]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
s : Set E
f g : E → β
inst✝ : SemilatticeSup β
hf : QuasiconvexOn 𝕜 s f
hg : QuasiconvexOn 𝕜 s g
r : β
⊢ Convex 𝕜 {x | x ∈ s ∧ f x ≤ r ∧ g x ≤ r}

Tactic:
Set.sep_and

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
s : Set E
f g : E → β
inst✝ : SemilatticeSup β
hf : QuasiconvexOn 𝕜 s f
hg : QuasiconvexOn 𝕜 s g
r : β
⊢ Convex 𝕜 ({x | x ∈ s ∧ f x ≤ r} ∩ {x | x ∈ s ∧ g x ≤ r})
Module: Mathlib.Analysis.Convex.Piecewise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝¹¹ : Semiring 𝕜
inst✝¹⁰ : PartialOrder 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : LinearOrder E
inst✝⁷ : IsOrderedAddMonoid E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : PosSMulMono 𝕜 E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConcaveOn 𝕜 (Set.Iic e) f
hg : ConcaveOn 𝕜 (Set.Ici e) g
h_mono : MonotoneOn f (Set.Iic e)
h_anti : AntitoneOn g (Set.Ici e)
h_eq : f e = g e
⊢ ConcaveOn 𝕜 Set.univ ((Set.Iic e).piecewise f g)

Tactic:
by
  rw [← neg_convexOn_iff, ← Set.piecewise_neg]
  exact convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici
    hf.neg hg.neg h_mono.neg h_anti.neg (neg_inj.mpr h_eq)

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
⊢ s.SOppSide x y ↔ s.SOppSide y x

Tactic:
rw [SOppSide, SOppSide, wOppSide_comm, and_comm (b := x ∉ s)]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.SSameSide y x ↔ s.SSameSide x y

Tactic:
sSameSide_comm

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.SSameSide x y ↔ s.SSameSide x y
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y z : P
h : Wbtw R x y z
hy : y ∈ s
⊢ s.WOppSide x z

Tactic:
rcases h with ⟨t, ⟨ht0, ht1⟩, rfl⟩

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : (lineMap x z) t ∈ s
⊢ s.WOppSide x z
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp.inr.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
hr : r₁ • (x -ᵥ p₁') = r₂ • (y -ᵥ p₂')
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
refine Or.inr ⟨(r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂', s.smul_vsub_vadd_mem _ h hp₁' hp₂',
        Or.inr (Or.inr ⟨r₁, r₂, hr₁, hr₂, ?_⟩)⟩
      rw [vsub_vadd_eq_vsub_sub, smul_sub, ← hr, smul_smul, mul_div_cancel₀ _ hr₂.ne.symm,
        ← smul_sub, vsub_sub_vsub_cancel_right]

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

Goal state before:
pp: case inr.inr.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
⊢ 0 ≤ bz * au / (az * av + bz * au)

pp: case inr.inr.refine_3
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
⊢ az * av / (az * av + bz * au) + bz * au / (az * av + bz * au) = 1

pp: case inr.inr.refine_4
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
⊢ (az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q) ∈
    (convexHull 𝕜) {p, q, az • x + bz • y}

Tactic:
· positivity

Goal state after:
case inr.inr.refine_3
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
⊢ az * av / (az * av + bz * au) + bz * au / (az * av + bz * au) = 1

case inr.inr.refine_4
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
⊢ (az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q) ∈
    (convexHull 𝕜) {p, q, az • x + bz • y}
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
⊢ dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c

Tactic:
have :
      dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔
        b -ᵥ a ∈ segment ℝ (a -ᵥ a) (c -ᵥ a) := by
    simp only [mem_segment_iff_sameRay, sameRay_iff_norm_add, dist_eq_norm', sub_add_sub_cancel',
      eq_comm]

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
this : dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔ b -ᵥ a ∈ [a -ᵥ a -[ℝ] c -ᵥ a]
⊢ dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c
Module: Mathlib.Analysis.Convex.StoneSeparation

Goal state before:
pp: case inr.inr.refine_4
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
z : Fin 3 → E := ![p, q, az • x + bz • y]
hw₀ : ∀ (i : Fin 3), 0 ≤ w i
hw : ∑ i, w i = az * av + bz * au
hz : ∀ (i : Fin 3), z i ∈ {p, q, az • x + bz • y}
⊢ (az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q) ∈
    (convexHull 𝕜) {p, q, az • x + bz • y}

Tactic:
convert!
      (Finset.centerMass_mem_convexHull (Finset.univ : Finset (Fin 3)) (fun i _ => hw₀ i)
          (by rwa [hw]) fun i _ => hz i :
        Finset.univ.centerMass w z ∈ _)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
z : Fin 3 → E := ![p, q, az • x + bz • y]
hw₀ : ∀ (i : Fin 3), 0 ≤ w i
hw : ∑ i, w i = az * av + bz * au
hz : ∀ (i : Fin 3), z i ∈ {p, q, az • x + bz • y}
⊢ (az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q) =
    Finset.univ.centerMass w z
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w : Fin (n + 1) → R
hw : ∑ j, w j = 1
i : Fin (n + 1)
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide (s.points i)
      ((Finset.affineCombination R Finset.univ s.points) w) ↔
    0 < w i

Tactic:
rw [← Finset.univ.affineCombination_piSingle R s.points (Finset.mem_univ i),
    s.sSameSide_affineSpan_faceOpposite_iff (Fintype.sum_pi_single' _ _) hw, eq_comm]
  simp [sign_eq_one_iff]

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

Goal state before:
pp: case e'_3.refine_3
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᵐ[μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ∞
aux :
  ∫ (a : ℝ) in Ioi 0, μ.real {a_1 | a < f a_1} = (∫⁻ (a : ℝ) in Ioi 0, ENNReal.ofReal (μ.real {a_1 | a < f a_1})).toReal
⊢ ∫ (t : ℝ) in Ioi 0, μ.real {a | t < f a} = (∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}).toReal

Tactic:
rw [aux]
      congr 1
      apply setLIntegral_congr_fun measurableSet_Ioi
      exact fun t t_pos ↦ ENNReal.ofReal_toReal (rhs_integrand_finite t t_pos).ne

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
⊢ ‖T‖ = ⨆ x, |T.rayleighQuotient x|

Tactic:
set M := ⨆ x, |T.rayleighQuotient x|
  have nonneg : 0 ≤ M := le_ciSup_of_le T.bddAbove_rayleighQuotient 0 (abs_nonneg _)
  have hM x : |re ⟪T x, x⟫| ≤ M * ‖x‖ ^ 2 := by
    have hM : |T.rayleighQuotient x| ≤ M := le_ciSup T.bddAbove_rayleighQuotient x
    by_cases hx : 0 < ‖x‖ ^ 2
    · rwa [rayleighQuotient, abs_div, abs_sq, reApplyInnerSelf, div_le_iff₀ hx] at hM
    · simp_all
  refine le_antisymm ?_ (ciSup_le T.rayleighQuotient_le_norm)
  refine opNorm_le_of_re_inner_le nonneg fun x y hx hy ↦ ?_
  transitivity M * (‖x + y‖ ^ 2 + ‖x - y‖ ^ 2) / 4
  · have key := congrArg re (add_conj ⟪T x, y⟫)
    rw [map_add, conj_inner_symm, ← coe_coe, ← hT, coe_coe, re_mul_ofReal, ofNat_re] at key
    grind [inner_add_left, inner_add_right, inner_sub_left, inner_sub_right]
  · rw [parallelogram_law_with_norm 𝕜 x y, hx, hy]
    grind

Goal state after:
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case h₁.hx1
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : x ≤ 1
⊢ 0 < (1 + x) / 2

pp: case h₁.hx2
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : x ≤ 1
⊢ (1 + x) / 2 ≤ 1

pp: case h₁.hz
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : x ≤ 1
⊢ -↑l ≤ 0

Tactic:
· positivity

Goal state after:
case h₁.hx2
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : x ≤ 1
⊢ (1 + x) / 2 ≤ 1

case h₁.hz
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : x ≤ 1
⊢ -↑l ≤ 0
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: case hab
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : x₀ ∈ sphere 0 ‖x₀‖
x : E
hx : x ∈ sphere 0 ‖x₀‖
this : ‖x‖ = ‖x₀‖
⊢ T.reApplyInnerSelf x ≤ T.reApplyInnerSelf x₀

Tactic:
exact hextr hx

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: case hab
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : x₀ ∈ sphere 0 ‖x₀‖
x : E
hx : x ∈ sphere 0 ‖x₀‖
this : ‖x‖ = ‖x₀‖
⊢ T.reApplyInnerSelf x₀ ≤ T.reApplyInnerSelf x

Tactic:
exact hextr hx

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Sort

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Equiv.refl (Fin n) = sort f ↔ Monotone f

Tactic:
eq_sort_iff,

Goal state after:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ (Monotone (f ∘ ⇑(Equiv.refl (Fin n))) ∧
      ∀ (i j : Fin n),
        i < j →
          f ((Equiv.refl (Fin n)) i) = f ((Equiv.refl (Fin n)) j) → (Equiv.refl (Fin n)) i < (Equiv.refl (Fin n)) j) ↔
    Monotone f
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
hμ : HasEigenvalue T μ
⊢ (starRingEnd 𝕜) μ = μ

Tactic:
obtain ⟨v, hv₁, hv₂⟩ := hμ.exists_hasEigenvector

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
hμ : HasEigenvalue T μ
v : E
hv₁ : v ∈ (genEigenspace T μ) 1
hv₂ : v ≠ 0
⊢ (starRingEnd 𝕜) μ = μ
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : IsSelfAdjoint a
⊢ ∃ φ,
    Continuous[_, instTopologicalSpaceMatrix] ⇑φ ∧
      Function.Injective ⇑φ ∧
        φ (ContinuousMap.restrict (spectrum ℝ a) (ContinuousMap.id ℝ)) = a ∧
          (∀ (f : C(↑(spectrum ℝ a), ℝ)), spectrum ℝ (φ f) = Set.range ⇑f) ∧
            ∀ (f : C(↑(spectrum ℝ a), ℝ)), IsSelfAdjoint (φ f)

Tactic:
replace ha : IsHermitian a := ha

Goal state after:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
⊢ ∃ φ,
    Continuous[_, instTopologicalSpaceMatrix] ⇑φ ∧
      Function.Injective ⇑φ ∧
        φ (ContinuousMap.restrict (spectrum ℝ a) (ContinuousMap.id ℝ)) = a ∧
          (∀ (f : C(↑(spectrum ℝ a), ℝ)), spectrum ℝ (φ f) = Set.range ⇑f) ∧
            ∀ (f : C(↑(spectrum ℝ a), ℝ)), IsSelfAdjoint (φ f)
Module: Mathlib.Analysis.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x y : n → 𝕜
⊢ star (M *ᵥ x) ⬝ᵥ y = M *ᵥ y ⬝ᵥ star x

Tactic:
star_mulVec,

Goal state after:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x y : n → 𝕜
⊢ star x ᵥ* Mᴴ ⬝ᵥ y = M *ᵥ y ⬝ᵥ star x
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
⊢ cfc f A = hA.cfc f

Tactic:
have hA' : IsSelfAdjoint A := hA

Goal state after:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
⊢ cfc f A = hA.cfc f
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re ⟪x, T x⟫
⊢ 0 ≤ μ

Tactic:
obtain ⟨v, hv₁, hv₂⟩ := hμ.exists_hasEigenvector

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re ⟪x, T x⟫
v : E
hv₁ : v ∈ (genEigenspace T ↑μ) 1
hv₂ : v ≠ 0
⊢ 0 ≤ μ
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < RCLike.re ⟪x, T x⟫
⊢ 0 < μ

Tactic:
obtain ⟨v, hv₁, hv₂⟩ := hμ.exists_hasEigenvector

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < RCLike.re ⟪x, T x⟫
v : E
hv₁ : v ∈ (genEigenspace T ↑μ) 1
hv₂ : v ≠ 0
⊢ 0 < μ
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: case refine_1
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
h : A.PosSemidef
a : 𝕜
⊢ a ∈ spectrum 𝕜 A → a ∈ {a | 0 ≤ a}

Tactic:
simp only [h.isHermitian.spectrum_eq_image_range, Set.mem_image, Set.mem_range,
      exists_exists_eq_and, Set.mem_ofPred_eq, forall_exists_index]

Goal state after:
case refine_1
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
h : A.PosSemidef
a : 𝕜
⊢ ∀ (x : n), ↑(⋯.eigenvalues x) = a → 0 ≤ a
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓^{n}_{K}(E, F)
this : (∀ (x : E), ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C) ↔ ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C
hi : ¬↑i ≤ n
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) f ≤ C ↔ ↑i ≤ n → ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C

Tactic:
· push Not at hi
    simp [hi, ContDiffMapSupportedIn.seminorm_eq_bot_of_gt _ hi, hC]

Goal state after: