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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
hull_sub_span : ↑(hull ℝ s) ⊆ ↑(Submodule.span ℝ s)
b : Basis ↑s ℝ E := Basis.mk hs_lin ⋯
⊢ C₁.minTensorProduct ↑C₂ = C₁.maxTensorProduct ↑C₂

Tactic:
have h_coord_dual : ∀ i, b.coord i ∈ dual (Dual.eval ℝ E) C₁ :=
    basis_coord_mem_dual _ _ (hs_span ▸ (Submodule.span_mono <| by simp [b]))

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
hull_sub_span : ↑(hull ℝ s) ⊆ ↑(Submodule.span ℝ s)
b : Basis ↑s ℝ E := Basis.mk hs_lin ⋯
h_coord_dual : ∀ (i : ↑s), b.coord i ∈ dual (Dual.eval ℝ E) ↑C₁
⊢ C₁.minTensorProduct ↑C₂ = C₁.maxTensorProduct ↑C₂
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this✝ : Filter.Tendsto (fun y ↦ 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
this : 2 * f x₀ ≤ f y + f (2 • x₀ - y)
⊢ 2 * f x₀ ≤ f y + f (2 • x₀ - y)

Tactic:
← Nat.cast_two,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this✝ : Filter.Tendsto (fun y ↦ 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
this : ↑2 * f x₀ ≤ f y + f (↑2 • x₀ - y)
⊢ 2 * f x₀ ≤ f y + f (2 • x₀ - y)
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst✝ : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᵐ[μ] g
this✝ : SeparableSpace ↑(range g ∩ s)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto (fun n ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
⊢ ∀ i ∈ (G n).range, 0 ≤ μ.real (⇑(G n) ⁻¹' {i})

Tactic:
exact fun _ _ => ENNReal.toReal_nonneg

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

Goal state before:
pp: f : ℝ → ℝ
y z : ℝ
hf_cnv : ConcaveOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
⊢ ContinuousOn f (Icc y z)

Tactic:
by
  simpa using hf_cnv.neg.continuousOn_Icc hyz hfy.neg hfz.neg

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

Goal state before:
pp: case e_b
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst✝ : IsStrictOrderedRing R
a : R
ha : a ≠ 0
hwa : w.weights = Finsupp.single x a
⊢ a = 1

Tactic:
simpa [hwa] using w.total

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

Goal state before:
pp: case singleton
K : Type u_4
X : Type u_5
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t : Finset X
x : X
w : StdSimplex K X
hw : ↑{x} ⊆ s
hsw : {x} = w.weights.support
⊢ sConvexComb w ∈ s

Tactic:
simp_all [eq_comm]

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✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f : E → β
⊢ ((∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ max (f x) (f y)) ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → min (f x) (f y) ≤ f (a • x + b • y)) ↔
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)

Tactic:
← forall_and,

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f : E → β
⊢ (∀ x ∈ s,
      ∀ x_2 ∈ s,
        ∀ (x_4 x_5 : 𝕜),
          0 ≤ x_4 →
            0 ≤ x_5 →
              x_4 + x_5 = 1 →
                f (x_4 • x + x_5 • x_2) ≤ max (f x) (f x_2) ∧ min (f x) (f x_2) ≤ f (x_4 • x + x_5 • x_2)) ↔
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)
Module: Mathlib.Analysis.Convex.Piecewise

Goal state before:
pp: case pos
𝕜 : 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 : ConvexOn 𝕜 (Set.Ici e) f
hg : ConvexOn 𝕜 (Set.Iic e) g
h_mono : MonotoneOn f (Set.Ici e)
h_anti : AntitoneOn g (Set.Iic e)
h_eq : f e = g e
x : E
hx : x = e
⊢ (Set.Ici e).piecewise f g x = (Set.Iic e).piecewise g f x

Tactic:
simp [Set.piecewise, @le_iff_lt_or_eq _ _ x e, ← @ite_not _ (e ≤ _), hx, h_eq]

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

Goal state before:
pp: case neg
𝕜 : 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 : ConvexOn 𝕜 (Set.Ici e) f
hg : ConvexOn 𝕜 (Set.Iic e) g
h_mono : MonotoneOn f (Set.Ici e)
h_anti : AntitoneOn g (Set.Iic e)
h_eq : f e = g e
x : E
hx : ¬x = e
⊢ (Set.Ici e).piecewise f g x = (Set.Iic e).piecewise g f x

Tactic:
simp [Set.piecewise, @le_iff_lt_or_eq _ _ x e, ← @ite_not _ (e ≤ _), hx, h_eq]

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

Goal state before:
pp: case neg
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : ↥s → E := ⋯
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i : ↥s
this : ∀ (J : Set ↥s), i ∈ J → (convexHull 𝕜) (a '' Jᶜ) ⊆ F ↑i
h : i ∉ I
⊢ p ∈ (convexHull 𝕜) (a '' Iᶜᶜ)

Tactic:
rwa [compl_compl]

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

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q u x y : E
hu : u ∈ segment 𝕜 x p
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
bv : 𝕜
hbv : 0 ≤ bv
hav : 0 ≤ 0
habv : 0 + bv = 1
⊢ ∃ x_1 ∈ segment 𝕜 u (0 • y + bv • q), x_1 ∈ (convexHull 𝕜) {p, q, az • x + bz • y}

Tactic:
rw [zero_add] at habv

Goal state after:
case inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q u x y : E
hu : u ∈ segment 𝕜 x p
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
bv : 𝕜
hbv : 0 ≤ bv
hav : 0 ≤ 0
habv : bv = 1
⊢ ∃ x_1 ∈ segment 𝕜 u (0 • y + bv • q), x_1 ∈ (convexHull 𝕜) {p, q, az • x + bz • y}
Module: Mathlib.Analysis.Convex.Strong

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
⊢ StrictConcaveOn ℝ s f

Tactic:
by
  refine ⟨hf.1, fun x hx y hy hxy a b ha hb hab ↦ (hf.2 hx hy ha.le hb.le hab).trans_lt' <|
    lt_add_of_pos_right _ ?_⟩
  rw [← sub_ne_zero, ← norm_pos_iff] at hxy
  positivity [hφ _ hxy.ne']

Goal state after:
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 p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (p₂ -ᵥ y)
⊢ r₂⁻¹ • -(r₂ • (p₂ -ᵥ y)) +ᵥ p₂ = y

Tactic:
smul_neg,

Goal state after:
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 p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (p₂ -ᵥ y)
⊢ -(r₂⁻¹ • r₂ • (p₂ -ᵥ y)) +ᵥ p₂ = y
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp
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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ s.WOppSide x y → ∃ a ≤ 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
rw [wOppSide_iff_exists_left hp, or_iff_right hx]
    rintro ⟨p₂, hp₂, h | h | ⟨r₁, r₂, hr₁, hr₂, h⟩⟩
    · rw [vsub_eq_zero_iff_eq] at h
      exact False.elim (hx (h.symm ▸ hp))
    · rw [vsub_eq_zero_iff_eq] at h
      refine ⟨0, le_rfl, p₂, hp₂, ?_⟩
      simp [h]
    · refine ⟨-r₁ / r₂, (div_neg_of_neg_of_pos (Left.neg_neg_iff.2 hr₁) hr₂).le, p₂, hp₂, ?_⟩
      rw [div_eq_inv_mul, ← smul_smul, neg_smul, h, smul_neg, smul_smul,
        inv_mul_cancel₀ hr₂.ne.symm, one_smul, neg_vsub_eq_vsub_rev, vsub_vadd]

Goal state after:
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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (p₂ -ᵥ y)
⊢ r₂⁻¹ • -(r₂ • (p₂ -ᵥ y)) +ᵥ p₂ = y

Tactic:
smul_neg,

Goal state after:
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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (p₂ -ᵥ y)
⊢ -(r₂⁻¹ • r₂ • (p₂ -ᵥ y)) +ᵥ p₂ = y
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case pos
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty ↥s
hx : x ∈ s
⊢ IsConnected {y | s.WSameSide x y}

pp: case neg
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty ↥s
hx : x ∉ s
⊢ IsConnected {y | s.WSameSide x y}

Tactic:
· simp only [wSameSide_of_left_mem, hx]
    have := AddTorsor.connectedSpace V P
    exact isConnected_univ

Goal state after:
case neg
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty ↥s
hx : x ∉ s
⊢ IsConnected {y | s.WSameSide x y}
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
this : Nonempty ↥s
⊢ IsConnected ((fun x_1 ↦ x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' Set.Ioi 0 ×ˢ ↑s)

Tactic:
refine (isConnected_Ioi.prod (isConnected_iff_connectedSpace.2 ?_)).image _
    ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn

Goal state after:
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
this : Nonempty ↥s
⊢ ConnectedSpace ↑↑s
Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ Integrable (fun x ↦ (1 + ‖x‖) ^ (-r)) μ

Tactic:
constructor
  · apply Measurable.aestronglyMeasurable (by fun_prop)
  -- Lower Lebesgue integral
  have : (∫⁻ a : E, ‖(1 + ‖a‖) ^ (-r)‖ₑ ∂μ) = ∫⁻ a : E, ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ :=
    lintegral_enorm_of_nonneg fun _ => rpow_nonneg (by positivity) _
  rw [hasFiniteIntegral_iff_enorm, this]
  exact finite_integral_one_add_norm hnr

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
⊢ ∀ (i : ℕ), ν ({a | f a ≤ M} ∪ {a | u i < f a}) < ∞

Tactic:
intro n
        have I : ν {a | f a ≤ M} = 0 := by
          rw [Measure.restrict_apply (measurableSet_le f_mble measurable_const)]
          convert! measure_empty (μ := μ)
          rw [← disjoint_iff_inter_eq_empty]
          exact disjoint_left.mpr (fun a ha ↦ by simpa using ha)
        have J : μ {a | u n < f a} < ∞ := by
          rw [lt_top_iff_ne_top]
          apply H2 _ (M_nonneg.trans_lt (uM n))
          by_contra H3
          rw [not_lt, intervalIntegral.integral_of_le (M_nonneg.trans (uM n).le)] at H3
          have g_nn_ae : ∀ᵐ t ∂(volume.restrict (Ioc 0 (u n))), 0 ≤ g t := by
            filter_upwards [ae_restrict_mem measurableSet_Ioc] with s hs using g_nn _ hs.1
          have Ig : ∫ (t : ℝ) in Ioc 0 (u n), g t = 0 :=
            le_antisymm H3 (integral_nonneg_of_ae g_nn_ae)
          have J : ∀ᵐ t ∂(volume.restrict (Ioc 0 (u n))), g t = 0 :=
            (integral_eq_zero_iff_of_nonneg_ae g_nn_ae
              (g_intble (u n) (M_nonneg.trans_lt (uM n))).1).1 Ig
          have : u n ≤ M := le_csSup M_bdd J
          exact lt_irrefl _ (this.trans_lt (uM n))
        refine lt_of_le_of_lt (measure_union_le _ _) ?_
        rw [I, zero_add]
        apply lt_of_le_of_lt _ J
        exact restrict_le_self _

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
inst✝⁹ : NormedSpace 𝕜 F
n : ℕ∞
V : Type u_6
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
t : TopologicalSpace V
inst✝⁶ : IsTopologicalAddGroup V
inst✝⁵ : ContinuousSMul ℝ V
inst✝⁴ : LocallyConvexSpace ℝ V
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F
inst✝¹ : Module 𝕜 V
inst✝ : IsScalarTower ℝ 𝕜 V
f : 𝓓^{n}(Ω, F) →ₗ[𝕜] V
this✝¹ : IsTopologicalAddGroup 𝓓^{n}(Ω, F)
this✝ : ContinuousSMul ℝ 𝓓^{n}(Ω, F)
this : LocallyConvexSpace ℝ 𝓓^{n}(Ω, F)
⊢ topologicalSpace Ω F n ≤ induced (⇑(↑ℝ f)) t ↔
    ∀ (K : Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω), Continuous[_, t] (⇑(↑ℝ f) ∘ ofSupportedIn K_sub_Ω)

Tactic:
simp_rw [topologicalSpace_le_iff, originalTop, iSup₂_le_iff, ← continuous_iff_le_induced,
    continuous_coinduced_dom]

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

Goal state before:
pp: case hf
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Differentiable ℝ _root_.id

Tactic:
apply differentiable_id

Goal state after:
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
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
f : C(↑(spectrum ℝ A), ℝ)
hf :
  ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary =
    0
⊢ diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩) = 0

Tactic:
replace hf := congr($hf * (hA.eigenvectorUnitary : Matrix n n 𝕜))

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
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
f : C(↑(spectrum ℝ A), ℝ)
hf :
  ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary *
      ↑hA.eigenvectorUnitary =
    0 * ↑hA.eigenvectorUnitary
⊢ diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩) = 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
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator ⇑T
hT' : (↑T).IsSymmetric
S : ↥(⨆ μ, eigenspace (↑T) μ)ᗮ →L[𝕜] ↥(⨆ μ, eigenspace (↑T) μ)ᗮ := T.restrict ⋯
hS_compact : IsCompactOperator ⇑S
hS_symm : (↑S).IsSymmetric
hS : ∀ (μ : 𝕜), eigenspace (↑S) μ = ⊥
h : ∀ (μ : 𝕜), HasEigenvalue (↑S) μ → μ = 0
⊢ (⨆ μ, eigenspace (↑T) μ)ᗮ = ⊥

Tactic:
rw [eq_zero_of_forall_hasEigenvalue_eq_zero hS_compact hS_symm] at h

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator ⇑T
hT' : (↑T).IsSymmetric
S : ↥(⨆ μ, eigenspace (↑T) μ)ᗮ →L[𝕜] ↥(⨆ μ, eigenspace (↑T) μ)ᗮ := T.restrict ⋯
hS_compact : IsCompactOperator ⇑S
hS_symm : (↑S).IsSymmetric
hS : ∀ (μ : 𝕜), eigenspace (↑S) μ = ⊥
h : S = 0
⊢ (⨆ μ, eigenspace (↑T) μ)ᗮ = ⊥
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹⁶ : NonUnitalRing A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Module ℝ A
inst✝¹² : SMulCommClass ℝ A A
inst✝¹¹ : IsScalarTower ℝ A A
inst✝¹⁰ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁹ : PartialOrder A
inst✝⁸ : StarOrderedRing A
inst✝⁷ : NonnegSpectrumClass ℝ A
inst✝⁶ : IsTopologicalRing A
inst✝⁵ : T2Space A
inst✝⁴ : StarModule ℝ A
R : Type u_3
inst✝³ : Semiring R
inst✝² : SMulWithZero R ℝ≥0
inst✝¹ : SMul R A
inst✝ : IsScalarTower R ℝ≥0 A
r : R
a : A
this : ∀ (r : ℝ≥0), abs (r • a) = r • abs a
⊢ abs (r • a) = r • abs a

Tactic:
simpa using this (r • 1)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝¹⁸ : RCLike 𝕜
inst✝¹⁷ : NonUnitalRing A
inst✝¹⁶ : TopologicalSpace A
inst✝¹⁵ : Module 𝕜 A
inst✝¹⁴ : StarRing A
inst✝¹³ : PartialOrder A
inst✝¹² : StarOrderedRing A
inst✝¹¹ : IsScalarTower 𝕜 A A
inst✝¹⁰ : SMulCommClass 𝕜 A A
inst✝⁹ : Module ℝ A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : IsScalarTower ℝ A A
inst✝⁶ : NonnegSpectrumClass ℝ A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : StarModule 𝕜 A
inst✝¹ : StarModule ℝ A
inst✝ : IsScalarTower ℝ 𝕜 A
r : 𝕜
a : A
⊢ abs (r • a) = ‖r‖ • abs a

Tactic:
trans abs (‖r‖ • a)
  · simp only [abs, mul_smul_comm, smul_mul_assoc, star_smul, ← smul_assoc,
      RCLike.real_smul_eq_coe_smul (K := 𝕜)]
    simp [-algebraMap_smul, ← smul_mul_assoc, ← mul_comm (starRingEnd _ _), RCLike.conj_mul, sq]
  · lift ‖r‖ to ℝ≥0 using norm_nonneg _ with r
    simp [← NNReal.smul_def]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: case pos
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖g x‖ = g x
gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖
x : α
hv : x ∈ v \ s ∪ s
⊢ ‖g x • c - s.indicator (fun _x ↦ c) x‖ ≤ ‖(v \ s).indicator (fun _x ↦ c) x‖

Tactic:
rcases hv with hsv | hs

Goal state after:
case pos.inl
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv✝ : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖g x‖ = g x
gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖
x : α
hsv : x ∈ v \ s
⊢ ‖g x • c - s.indicator (fun _x ↦ c) x‖ ≤ ‖(v \ s).indicator (fun _x ↦ c) x‖

case pos.inr
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs✝ : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖g x‖ = g x
gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖
x : α
hs : x ∈ s
⊢ ‖g x • c - s.indicator (fun _x ↦ c) x‖ ≤ ‖(v \ s).indicator (fun _x ↦ c) x‖