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

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✝ : AddTorsor V P
x y z : P
⊢ Sbtw R x y z ↔ x ≠ y ∧ z ∈ ⇑(lineMap x y) '' Set.Ioi 1

Tactic:
by
  refine ⟨fun h => ⟨h.left_ne, ?_⟩, fun h => ?_⟩
  · obtain ⟨r, ⟨hr, rfl⟩⟩ := h.wbtw.right_mem_image_Ici_of_left_ne h.left_ne
    rw [Set.mem_Ici] at hr
    rcases hr.lt_or_eq with (hrlt | rfl)
    · exact Set.mem_image_of_mem _ hrlt
    · simp at h
  · rcases h with ⟨hne, r, hr, rfl⟩
    rw [Set.mem_Ioi] at hr
    refine
      ⟨wbtw_iff_left_eq_or_right_mem_image_Ici.2
          (Or.inr (Set.mem_image_of_mem _ (Set.mem_of_mem_of_subset hr Set.Ioi_subset_Ici_self))),
        hne.symm, ?_⟩
    rw [lineMap_apply, ← @vsub_ne_zero V, vsub_vadd_eq_vsub_sub]
    nth_rw 1 [← one_smul R (y -ᵥ x)]
    rw [← sub_smul, smul_ne_zero_iff, vsub_ne_zero, sub_ne_zero]
    exact ⟨hr.ne, hne.symm⟩

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
s : AffineSubspace R P
hxyz : Wbtw R x y z
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
⊢ z ∈ s

Tactic:
by
  obtain ⟨ε, -, rfl⟩ := hxyz
  have hε : ε ≠ 0 := by rintro rfl; simp at hxy
  simpa [hε] using lineMap_mem ε⁻¹ hx hy

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

Goal state before:
pp: case refine_5
𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
t' : Finset E := {i ∈ t | w i ≠ 0}
⊢ ∑ i, (w ∘ Subtype.val) i • ↑i = x

Tactic:
change (∑ i ∈ t'.attach, (fun e => w e • e) ↑i) = x

Goal state after:
case refine_5
𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
t' : Finset E := {i ∈ t | w i ≠ 0}
⊢ ∑ i ∈ t'.attach, (fun e ↦ w e • e) ↑i = x
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ∀ (y : F), (ContinuousLinearMap.adjoint f) y ∈ innerDual ↑C → 0 ≤ ⟪b, y⟫_ℝ
⊢ b ∈ map f C

Tactic:
by
    -- By contradiction, suppose `b ∉ C.map f`.
    contrapose! h
    -- as `b ∉ C.map f`, there is a hyperplane `y` separating `b` from `C.map f`
    obtain ⟨y, hxy, hyb⟩ := (C.map f).hyperplane_separation' h
    -- the rest of the proof is a straightforward algebraic manipulation
    refine ⟨y, fun x hx ↦ ?_, hyb⟩
    simpa [ContinuousLinearMap.adjoint_inner_right]
      using hxy (f x) (subset_closure <| mem_image_of_mem _ hx)

Goal state after:
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
x : E
c : E →₀ ℝ
hc_supp : ↑c.support ⊆ s
left✝ : ∀ (y : E), 0 ≤ c y
hc_sum : (c.sum fun m r ↦ r • m) = x
⊢ x ∈ ↑(Submodule.span ℝ s)

Tactic:
exact hc_sum ▸ Submodule.sum_mem _ fun m hm =>
      Submodule.smul_mem _ _ (Submodule.subset_span (hc_supp hm))

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

Goal state before:
pp: case inr
β : Type u_2
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
⊢ f a ≤ f c

Tactic:
suffices ya • f a + yc • f a ≤ ya • f a + yc • f c from
    (smul_le_smul_iff_of_pos_left yc₀).1 (le_of_add_le_add_left this)

Goal state after:
case inr
β : Type u_2
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
⊢ ya • f a + yc • f a ≤ ya • f a + yc • f c
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hr : r' < r
M : ℝ
hM : ∀ (a : E), dist a x₀ < r → |f a| < M
⊢ ∃ K, LipschitzOnWith K f (ball x₀ r')

Tactic:
rw [← sub_sub_cancel r r']

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hr : r' < r
M : ℝ
hM : ∀ (a : E), dist a x₀ < r → |f a| < M
⊢ ∃ K, LipschitzOnWith K f (ball x₀ (r - (r - r')))
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s t : Set E
x : E
⊢ x ∈ convexJoin 𝕜 s t ↔ ∃ a ∈ s, ∃ b ∈ t, x ∈ segment 𝕜 a b

Tactic:
simp [convexJoin]

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
t : Set E
⊢ convexJoin 𝕜 ∅ t = ∅

Tactic:
simp [convexJoin]

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ convexJoin 𝕜 s ∅ = ∅

Tactic:
simp [convexJoin]

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
t : Set E
x : E
⊢ convexJoin 𝕜 {x} t = ⋃ y ∈ t, segment 𝕜 x y

Tactic:
simp [convexJoin]

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
y : E
⊢ convexJoin 𝕜 s {y} = ⋃ x ∈ s, segment 𝕜 x y

Tactic:
simp [convexJoin]

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
hs : IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s)
⊢ intrinsicClosure 𝕜 s = s

Tactic:
rw [intrinsicClosure, hs.closure_eq, image_preimage_eq_of_subset]
  exact (subset_affineSpan _ _).trans Subtype.range_coe.superset

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
hs : IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s)
⊢ intrinsicClosure 𝕜 s = s

Tactic:
by
  rw [intrinsicClosure, hs.closure_eq, image_preimage_eq_of_subset]
  exact (subset_affineSpan _ _).trans Subtype.range_coe.superset

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

Goal state before:
pp: f : ℝ → ℝ
y z : ℝ
hf_cnv : ConcaveOn ℝ (Ioc y z) f
hf_cont : ContinuousWithinAt f (Iic z) z
⊢ ContinuousOn f (Ioc y z)

Tactic:
simpa using hf_cnv.neg.continuousOn_Ioc hf_cont.neg

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : AddCommGroup V
inst✝³ : Module 𝕜 V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousConstSMul 𝕜 V
s : Set V
hs : Convex 𝕜 s
⊢ Convex 𝕜 (intrinsicClosure 𝕜 s)

Tactic:
by
  rw [intrinsicClosure_eq_closure_inter_affineSpan]
  exact hs.closure.inter (affineSpan 𝕜 s).convex

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst✝ : IsFiniteMeasure μ
hg : StrictConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
t : Set α
hm : MeasurableSet t
h₀ : μ t ≠ 0
h₀' : μ tᶜ ≠ 0
hne : ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h_avg :
  a • ⨍ (x : α) in t, f x ∂μ + b • ⨍ (x : α) in tᶜ, f x ∂μ = ⨍ (x : α), f x ∂μ ∧
    a • ⨍ (x : α) in t, g (f x) ∂μ + b • ⨍ (x : α) in tᶜ, g (f x) ∂μ = ⨍ (x : α), g (f x) ∂μ
⊢ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ

Tactic:
rw [← h_avg.1, ← h_avg.2]

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst✝ : IsFiniteMeasure μ
hg : StrictConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
t : Set α
hm : MeasurableSet t
h₀ : μ t ≠ 0
h₀' : μ tᶜ ≠ 0
hne : ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h_avg :
  a • ⨍ (x : α) in t, f x ∂μ + b • ⨍ (x : α) in tᶜ, f x ∂μ = ⨍ (x : α), f x ∂μ ∧
    a • ⨍ (x : α) in t, g (f x) ∂μ + b • ⨍ (x : α) in tᶜ, g (f x) ∂μ = ⨍ (x : α), g (f x) ∂μ
⊢ g (a • ⨍ (x : α) in t, f x ∂μ + b • ⨍ (x : α) in tᶜ, f x ∂μ) <
    a • ⨍ (x : α) in t, g (f x) ∂μ + b • ⨍ (x : α) in tᶜ, g (f x) ∂μ
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
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
s : Set Y
hf : IsAffineMap R f
hs : IsConvexSet R s
⊢ IsConvexSet R (f ⁻¹' s)

Tactic:
rintro w hw
  simp only [mem_preimage, hf.map_sConvexComb, sConvexComb_map]
  exact hs.iConvexComb_mem fun x hx ↦ hw <| by simpa

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

Goal state before:
pp: case inl
ι : 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
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
h_card : #s < finrank 𝕜 E + 1
⊢ (⋂ i ∈ s, F i).Nonempty

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
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
h_card : finrank 𝕜 E + 1 ≤ #s
⊢ (⋂ i ∈ s, F i).Nonempty

Tactic:
· exact helly_theorem_corner (le_of_lt h_card) h_inter

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
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
h_card : finrank 𝕜 E + 1 ≤ #s
⊢ (⋂ i ∈ s, F i).Nonempty
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: case h_inter
𝕜 : 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
i : ↥s
⊢ ∀ I ⊆ s.erase ↑i, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty

Tactic:
intro J hJ_ss hJ_card
      exact h_inter J (subset_trans hJ_ss (erase_subset i.val s)) hJ_card

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

Goal state before:
pp: case hb
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
b : X × X
x y : ↑(Set.Icc 0 1)
⊢ edist (convexCombPair (↑(x, b).1) (1 - ↑(x, b).1) ⋯ ⋯ ⋯ (x, b).2.1 (x, b).2.2)
      (convexCombPair (↑(y, b).1) (1 - ↑(y, b).1) ⋯ ⋯ ⋯ (y, b).2.1 (y, b).2.2) ≤
    ↑(nndist b.1 b.2) * edist x y

Tactic:
mul_comm

Goal state after:
case hb
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
b : X × X
x y : ↑(Set.Icc 0 1)
⊢ edist (convexCombPair (↑(x, b).1) (1 - ↑(x, b).1) ⋯ ⋯ ⋯ (x, b).2.1 (x, b).2.2)
      (convexCombPair (↑(y, b).1) (1 - ↑(y, b).1) ⋯ ⋯ ⋯ (y, b).2.1 (y, b).2.2) ≤
    edist x y * ↑(nndist b.1 b.2)
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
⊢ K.vertices = ⋃ k ∈ K.faces, ↑k

Tactic:
ext x
  refine ⟨fun h => mem_biUnion h <| mem_coe.2 <| mem_singleton_self x, fun h => ?_⟩
  obtain ⟨s, hs, hx⟩ := mem_iUnion₂.1 h
  exact K.down_closed hs (Finset.singleton_subset_iff.2 <| mem_coe.1 hx) (singleton_nonempty _)

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

Goal state before:
pp: I : Type u_1
X : Type u_2
inst✝⁶ : ConvexSpace ℝ X
inst✝⁵ : MetricSpace X
inst✝⁴ : IsConvexDist X
V : Type u_3
P : Type u_4
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
f : StdSimplex ℝ (P × P)
p : P := ⋯.some
⊢ dist ((Finset.affineCombination ℝ f.weights.support Prod.fst) ⇑f.weights)
      ((Finset.affineCombination ℝ f.weights.support Prod.snd) ⇑f.weights) ≤
    iConvexComb f fun x ↦ dist x.1 x.2

Tactic:
rw [Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _ f.total p,
      Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _ f.total p]

Goal state after:
I : Type u_1
X : Type u_2
inst✝⁶ : ConvexSpace ℝ X
inst✝⁵ : MetricSpace X
inst✝⁴ : IsConvexDist X
V : Type u_3
P : Type u_4
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
f : StdSimplex ℝ (P × P)
p : P := ⋯.some
⊢ dist (((f.weights.support.weightedVSubOfPoint Prod.fst p) fun i ↦ (fun x r ↦ r) i (f.weights i)) +ᵥ p)
      (((f.weights.support.weightedVSubOfPoint Prod.snd p) fun i ↦ (fun x r ↦ r) i (f.weights i)) +ᵥ p) ≤
    iConvexComb f fun x ↦ dist x.1 x.2
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
inst✝¹ : Fintype V
inst✝ : DecidableEq V
⊢ ∀ (x : SimpleGraph V), x ∈ map SimpleGraph.mk' univ

Tactic:
rintro ⟨Adj, hs, hi⟩
    simp only [mem_map, mem_univ, true_and, Subtype.exists, Bool.not_eq_true]
    refine ⟨fun v w ↦ Adj v w, ⟨?_, ?_⟩, ?_⟩
    · simp [hs.iff]
    · intro v; simp [hi.irrefl v]
    · ext
      simp

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
⊢ Fintype ↑∅

Tactic:
infer_instance

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₁.edgeSet ∪ G₂.edgeSet)

Tactic:
infer_instance

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
s : Set (Sym2 V)
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑s
⊢ Fintype ↑(s \ Sym2.diagSet)

Tactic:
infer_instance

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
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t ≤ 0
⊢ s.WOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
refine ⟨p₂, hp₂, p₁, hp₁, ?_⟩
  rw [vadd_vsub, ← neg_neg t, neg_smul, ← smul_neg, neg_vsub_eq_vsub_rev]
  exact SameRay.sameRay_nonneg_smul_left _ (neg_nonneg.2 ht)

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f₁ f₂ : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ holder r B (f₁ + f₂) g = holder r B f₁ g + holder r B f₂ g

Tactic:
by
  simp only [holder, ← MemLp.toLp_add]
  apply MemLp.toLp_congr
  filter_upwards [AEEqFun.coeFn_add f₁.val f₂.val] with x hx
  simp [hx]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
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
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h : s ∉ Ioc 0 (f a)
⊢ (Ioc 0 (f a)).indicator (fun t ↦ ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x ↦ 1) s * (Ici s).indicator (fun x ↦ 1) (f a)

Tactic:
have h_copy := h
        simp only [mem_Ioc, not_and, not_le] at h
        by_cases h' : 0 < s
        · simp only [h_copy, h h', indicator_of_notMem, not_false_iff, mem_Ici, not_le, mul_zero]
        · have : s ∉ Ioi (0 : ℝ) := h'
          simp only [this, h', indicator_of_notMem, not_false_iff, mul_zero,
            zero_mul, mem_Ioc, false_and]

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

Goal state before:
pp: D : Type u_4
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup D
inst✝ : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ : ∀ (N : ℕ), ∃ k C, ∃ (_ : 0 ≤ C), ∀ n ≤ N, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n g t x‖ ≤ C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ : ∀ n_1 ≤ n, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n_1 g t x‖ ≤ C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * ↑(k₂.choose k) * C₁ ^ k
x : D
hg' : ∀ i ≤ n, ‖iteratedFDerivWithin ℝ i g t (f x)‖ ≤ C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
i : ℕ
hi : 1 ≤ i
hi' : i ≤ n
⊢ 1 ≤ (1 + ‖x‖) ^ k₁

Tactic:
simp [one_le_pow₀]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕂 : Type u_2
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
F' : Type u_5
inst✝¹¹ : NormedAddCommGroup F'
inst✝¹⁰ : NormedSpace ℝ F'
inst✝⁹ : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
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
toFun : 𝓓^{n}(Ω, F) → V
T : (K : Compacts E) → ↑K ⊆ ↑Ω → 𝓓^{n}_{K}(E, F) →L[𝕜] V
toFun_eq_T :
  ∀ (K : Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω) (f : 𝓓^{n}_{K}(E, F)), toFun (ofSupportedIn K_sub_Ω f) = (T K K_sub_Ω) f
toFun_add : ∀ (f g : 𝓓^{n}(Ω, F)), toFun (f + g) = toFun f + toFun g
c : 𝕜
f : 𝓓^{n}(Ω, F)
⊢ toFun (c • f) = c • toFun f

Tactic:
by
    set K : Compacts E := ⟨tsupport f, f.hasCompactSupport⟩
    have K_sub_Ω : (K : Set E) ⊆ Ω := f.tsupport_subset
    let f_K : 𝓓^{n}_{K}(E, F) := .of_support_subset f.contDiff subset_closure
    change toFun (ofSupportedIn K_sub_Ω (c • f_K)) = c • toFun (ofSupportedIn K_sub_Ω f_K)
    simp [toFun_eq_T]

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

Goal state before:
pp: α : 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} < ∞
⊢ ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Ioi 0, μ.real {a | t < f a}

Tactic:
convert! (ENNReal.toReal_eq_toReal_iff' lhs_finite.ne rhs_finite.ne).mpr key

Goal state after:
case e'_2
α : 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} < ∞
⊢ ∫ (ω : α), f ω ∂μ = (∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ).toReal

case e'_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} < ∞
⊢ ∫ (t : ℝ) in Ioi 0, μ.real {a | t < f a} = (∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}).toReal
Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty

Goal state before:
pp: case h
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
ε : ℝ
hε : ε > 0
hs : Metric.ball 0 ε ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
⊢ (Metric.closedBall 0 r)ᶜ ⊆ (fun x ↦ ‖f x‖) ⁻¹' s

Tactic:
intro

Goal state after:
case h
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
ε : ℝ
hε : ε > 0
hs : Metric.ball 0 ε ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
a✝ : E
⊢ a✝ ∈ (Metric.closedBall 0 r)ᶜ → a✝ ∈ (fun x ↦ ‖f x‖) ⁻¹' s