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

Goal state before:

Tactic:
ya • f a + yc • f a = f a := by rw [← add_smul, yac, one_smul]
    _ ≤ f (ya * a + yc * c) := hfy
    _ ≤ ya • f a + yc • f c := h_conv.2 (left_mem_Icc.2 a_lt_b.le) hc ya₀ yc₀.le yac

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

Goal state before:
pp: case hsc
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
⊢ Convex ℝ (-x +ᵥ s)

Tactic:
simp [← mem_interior_iff_mem_nhds, interior_vadd, mem_vadd_set_iff_neg_vadd_mem, *]

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

Goal state before:
pp: case hs₀
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
⊢ -x +ᵥ s ∈ 𝓝 0

Tactic:
simp [← mem_interior_iff_mem_nhds, interior_vadd, mem_vadd_set_iff_neg_vadd_mem, *]

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

Goal state before:
pp: case hsb
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
⊢ IsVonNBounded ℝ (-x +ᵥ s)

Tactic:
simp [← mem_interior_iff_mem_nhds, interior_vadd, mem_vadd_set_iff_neg_vadd_mem, *]

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

Goal state before:
pp: case htc
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
⊢ Convex ℝ (-y +ᵥ t)

Tactic:
simp [← mem_interior_iff_mem_nhds, interior_vadd, mem_vadd_set_iff_neg_vadd_mem, *]

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

Goal state before:
pp: case ht₀
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
⊢ -y +ᵥ t ∈ 𝓝 0

Tactic:
simp [← mem_interior_iff_mem_nhds, interior_vadd, mem_vadd_set_iff_neg_vadd_mem, *]

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

Goal state before:
pp: case htb
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
⊢ IsVonNBounded ℝ (-y +ᵥ t)

Tactic:
simp [← mem_interior_iff_mem_nhds, interior_vadd, mem_vadd_set_iff_neg_vadd_mem, *]

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

Goal state before:
pp: ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : ι → Set E
t : Set E
⊢ ⋃ x, ⋃ (_ : ∃ i, x ∈ s i), ⋃ y ∈ t, segment 𝕜 x y = ⋃ i, ⋃ x ∈ s i, ⋃ y ∈ t, segment 𝕜 x y

Tactic:
iUnion_exists

Goal state after:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : ι → Set E
t : Set E
⊢ ⋃ x, ⋃ i, ⋃ (_ : x ∈ s i), ⋃ y ∈ t, segment 𝕜 x y = ⋃ i, ⋃ x ∈ s i, ⋃ y ∈ t, segment 𝕜 x y
Module: Mathlib.Analysis.Convex.Measure

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : μ (interior s) ≠ ∞
d : ℕ := finrank ℝ E
r : ℝ≥0
hr : 1 < r
⊢ μ (⇑(AffineMap.homothety x ↑r) '' interior s) = ↑(r ^ d) * μ (interior s)

Tactic:
rw [addHaar_image_homothety, ← NNReal.coe_pow, NNReal.abs_eq, ENNReal.ofReal_coe_nnreal]

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

Goal state before:
pp: R✝ : Type u_1
X : Type u_2
M✝ : Type u_3
N✝ : Type u_4
P✝ : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
N : Type u_10
P : Type u_11
w : StdSimplex R M
x : M
inst✝ : IsStrictOrderedRing R
f : StdSimplex R (StdSimplex R M)
⊢ ((f.weights.sum fun d r ↦ r • d.weights).sum fun x r ↦ r) = 1

Tactic:
simp [sum_sum_index, sum_smul_index, ← mul_sum]

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

Goal state before:
pp: case inl.inr.inr
𝕜 : 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.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
x✝¹ : x ∈ Set.univ
y : E
x✝ : y ∈ Set.univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : e < a • x + b • y
hc' : a • x + b • y ≤ a • e + b • y
⊢ g (a • x + b • y) ≤ a • f x + b • g y

Tactic:
trans a • g e + b • g y

Goal state after:
𝕜 : 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.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
x✝¹ : x ∈ Set.univ
y : E
x✝ : y ∈ Set.univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : e < a • x + b • y
hc' : a • x + b • y ≤ a • e + b • y
⊢ g (a • x + b • y) ≤ a • g e + b • g y

𝕜 : 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.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
x✝¹ : x ∈ Set.univ
y : E
x✝ : y ∈ Set.univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : e < a • x + b • y
hc' : a • x + b • y ≤ a • e + b • y
⊢ a • g e + b • g y ≤ a • f x + b • g y
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_card : finrank 𝕜 E + 1 ≤ #F
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
I : Finset (Set E)
hI_ss : I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset (Set E)
left✝ : I ⊆ J
hJ_ss : J ⊆ F
hJ_card : #J = finrank 𝕜 E + 1
⊢ ↑I ⊆ ↑J

Tactic:
by simpa [hI_ss]

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

Goal state before:
pp: case inr
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), (⋂ i ∈ I, F i).Nonempty
i0 : ι
⊢ (⋂ i, F i).Nonempty

Tactic:
show ⋂ i, F i = (F i0) ∩ ⋂ i, F i by simp [iInter_subset]

Goal state after:
case inr
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), (⋂ i ∈ I, F i).Nonempty
i0 : ι
⊢ (F i0 ∩ ⋂ i, F i).Nonempty
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: case a
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
G : Finset ↑F
a✝ : #G ≤ finrank 𝕜 E + 1
G' : Finset (Set E) := ⋯
⊢ #G' ≤ finrank 𝕜 E + 1

Tactic:
· apply le_trans card_image_le
    assumption

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : Set (Set E)
h_card : ↑(finrank 𝕜 E) + 1 ≤ F.encard
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → #G = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
I : Finset (Set E)
hI_ss : ↑I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Set (Set E)
left✝ : ↑I ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = ↑(finrank 𝕜 E) + 1
⊢ ↑I ⊆ ?m.107

Tactic:
by simpa [hI_ss]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: ι : Sort u_1
V : Type u
G H : SimpleGraph V
a b c u v w : V
e : Sym2 V
G₁ G₂ : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ Fintype ↑(G₁ ⊔ G₂).edgeSet

Tactic:
edgeSet_sup

Goal state after:
ι : Sort u_1
V : Type u
G H : SimpleGraph V
a b c u v w : V
e : Sym2 V
G₁ G₂ : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ Fintype ↑(G₁.edgeSet ∪ G₂.edgeSet)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow

Goal state before:
pp: this : ⇑sqrt = fun x ↦ x ^ (1 / 2)
⊢ StrictConcaveOn ℝ≥0 univ ⇑sqrt

Tactic:
rw [this]

Goal state after:
this : ⇑sqrt = fun x ↦ x ^ (1 / 2)
⊢ StrictConcaveOn ℝ≥0 univ fun x ↦ x ^ (1 / 2)
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
⊢ (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:
have hz : ∀ i, z i ∈ ({p, q, az • x + bz • y} : Set E) := fun i => by fin_cases i <;> simp [z]

Goal state after:
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}
Module: Mathlib.Analysis.Convex.StrictCombination

Goal state before:
pp: V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
t : Finset ι
w : ι → ℝ
p₀ : P
r : ℝ
p : ι → P
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : ∑ i ∈ t, w i = 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : p i ≠ p j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hp : ∀ i ∈ t, dist (p i) p₀ ≤ r
⊢ dist ((t.weightedVSubOfPoint p p₀) w +ᵥ p₀) p₀ < r

Tactic:
weightedVSubOfPoint_apply,

Goal state after:
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
t : Finset ι
w : ι → ℝ
p₀ : P
r : ℝ
p : ι → P
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : ∑ i ∈ t, w i = 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : p i ≠ p j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hp : ∀ i ∈ t, dist (p i) p₀ ≤ r
⊢ dist (∑ i ∈ t, w i • (p i -ᵥ p₀) +ᵥ p₀) p₀ < r
Module: Mathlib.Analysis.Convex.Strong

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
⊢ StrongConcaveOn s m f ↔ ConcaveOn ℝ s fun x ↦ f x + m / 2 * ‖x‖ ^ 2

Tactic:
by
  refine and_congr_right fun _ ↦ forall₄_congr fun x _ y _ ↦ forall₅_congr fun a b ha hb hab ↦ ?_
  simp_rw [← sub_le_iff_le_add, smul_eq_mul, aux_add ha hb hab, mul_assoc, mul_left_comm]

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₂ • (y -ᵥ p₂)
⊢ ∃ a, 0 < a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
· refine ⟨r₁ / r₂, div_pos hr₁ hr₂, p₂, hp₂, ?_⟩
      rw [div_eq_inv_mul, ← smul_smul, h, smul_smul, inv_mul_cancel₀ hr₂.ne.symm, one_smul,
        vsub_vadd]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
x : E
hx : x ∉ Ω
f : 𝓓^{n}(Ω, ℝ)
hx_support : x ∉ tsupport ⇑f
⊢ f x = 0

Tactic:
exact image_eq_zero_of_notMem_tsupport hx_support

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}
this : SigmaFinite ν
meas : MeasurableSet {a | M < f a}
s : α
hs : s ∈ {a | M < f a}ᶜ
⊢ ∫ (t : ℝ) in 0..f s, g t = ∫ (t : ℝ) in 0..f s, 0

Tactic:
simp_rw [intervalIntegral.integral_of_le (f_nonneg s)]

Goal state after:
α : 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}
this : SigmaFinite ν
meas : MeasurableSet {a | M < f a}
s : α
hs : s ∈ {a | M < f a}ᶜ
⊢ ∫ (t : ℝ) in Ioc 0 (f s), g t ∂volume = ∫ (t : ℝ) in Ioc 0 (f s), 0 ∂volume
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₁ n₂ : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n₁}(Ω₁, F)
⊢ ⇑((monoCLM 𝕜) f) = ⇑(if n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then f else 0)

Tactic:
monoCLM

Goal state after:
𝕜 : 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₁ n₂ : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n₁}(Ω₁, F)
⊢ ⇑((TestFunction.limitCLM 𝕜
          (fun f ↦
            if h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then
              { toFun := ⇑f, contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }
            else 0)
          (fun K K_sub_Ω₁ ↦
            if h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then ofSupportedInCLM 𝕜 ⋯ ∘SL ContDiffMapSupportedIn.monoCLM 𝕜 else 0)
          ⋯)
        f) =
    ⇑(if n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then f else 0)
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case h'f
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ HasTemperateGrowth (fderiv ℝ _root_.id)

Tactic:
convert Function.HasTemperateGrowth.const (ContinuousLinearMap.id ℝ E)
    exact fderiv_fun_id

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
inst✝ : Nontrivial E
hT' : (algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T
hT'' : -(algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T
ε : ℝ
hε0 : ε > 0
hε : ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε
ε' : ℝ
hε'0 : ε' > 0
hε' : ∀ (x : E), (-T).rayleighQuotient x ≤ ‖-T‖ - ε'
⊢ ∃ ε > 0, ∀ (x : E), |T.rayleighQuotient x| ≤ ‖T‖ - ε

Tactic:
exact ⟨min ε ε', by grind, fun x ↦ by grind [rayleighQuotient_neg_apply, norm_neg]⟩

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

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : IsUniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U
⊢ TotallyBounded (⇑u '' closedBall 0 1)

Tactic:
rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero]

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : IsUniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U
⊢ ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ ⇑u '' closedBall 0 1 ⊆ ⋃ y ∈ t, y +ᵥ U
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: 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₂)
⊢ x ^ k * f ≤ 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l)

Tactic:
rw [this]

Goal state after:
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₂)
⊢ x ^ k * f ≤ ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

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 : 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 / ‖x‖ ^ 2 ≤ T.reApplyInnerSelf x₀ / ‖x₀‖ ^ 2

Tactic:
rw [this]

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 : 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 / ‖x₀‖ ^ 2 ≤ T.reApplyInnerSelf x₀ / ‖x₀‖ ^ 2
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

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 : 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₀ / ‖x₀‖ ^ 2 ≤ T.reApplyInnerSelf x / ‖x‖ ^ 2

Tactic:
rw [this]

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 : 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₀ / ‖x₀‖ ^ 2 ≤ T.reApplyInnerSelf x / ‖x₀‖ ^ 2
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A B : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : A.charpoly = B.charpoly
this : hA.eigenvalues₀ = hB.eigenvalues₀
⊢ (fun i ↦ hA.eigenvalues₀ ((Fintype.equivOfCardEq ⋯).symm i)) = fun i ↦
    hB.eigenvalues₀ ((Fintype.equivOfCardEq ⋯).symm i)

Tactic:
rw [this]

Goal state after:
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ A.trace = ∑ i, ↑(hA.eigenvalues i)

Tactic:
simp [trace_eq_sum_roots_charpoly_of_splits hA.splits_charpoly, hA.roots_charpoly_eq_eigenvalues]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
⊢ (if hk : k + 1 ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0) =
    (RingHom.id 𝕜) c • if hk : k + 1 ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0

Tactic:
split_ifs with hk
    · have hk' : 0 < (n : ℕ∞ω) := mod_cast (add_pos_of_right zero_lt_one k).trans_le hk
      ext
      simp [fderiv_const_smul (f.contDiff.differentiable hk'.ne').differentiableAt,
        FunLike.coe_smul]
    · simp

Goal state after: