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

Goal state before:
pp: case cons.refine_2.refine_1.cons.inl.cons
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
head head3 : P
tail : List P
x✝ :
  (Pairwise (Sbtw R head) (head :: head3 :: tail) ∧ Triplewise (Sbtw R) (head :: head3 :: tail)) ∧
    ∀ (a : P), head :: head :: head3 :: tail ≠ [a, a]
hp : (∀ a' ∈ head3 :: tail, Sbtw R head head a') ∧ Pairwise (Sbtw R head) (head3 :: tail)
ht : Triplewise (Sbtw R) (head :: head3 :: tail)
ha : ∀ (a : P), head :: head :: head3 :: tail ≠ [a, a]
ht' : List.Wbtw R (head :: head3 :: tail)
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: head3 :: tail) ↔ ∀ (a : P), head :: head3 :: tail ≠ [a, a]
ha' : head ∈ head :: head3 :: tail
⊢ False

Tactic:
simpa using hp.1 head3

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✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
x y : P
⊢ affineSegment R x y = affineSegment R y x

Tactic:
refine Set.ext fun z => ?_

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
x y z : P
⊢ z ∈ affineSegment R x y ↔ z ∈ affineSegment R y x
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z p : P
⊢ Wbtw R x y z ∧ y ≠ x ∧ y -ᵥ p ≠ z -ᵥ p ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z

Tactic:
(vsub_left_injective p).ne_iff

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z p : P
⊢ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : PartialOrder R
x : R
⊢ (0 ≤ x ∧ x ≤ 1) ∧ x ≠ 0 ∧ x ≠ 1 ↔ x ∈ Set.Ioo 0 1

Tactic:
Set.mem_Ioo

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : PartialOrder R
x : R
⊢ (0 ≤ x ∧ x ≤ 1) ∧ x ≠ 0 ∧ x ≠ 1 ↔ 0 < x ∧ x < 1
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x z : P
hxz : x ≠ z
t : R
ht : t ∈ Set.Ioo 0 1
⊢ (lineMap x z) t ≠ x ∧ (lineMap x z) t ≠ z

Tactic:
rw [lineMap_apply, ← @vsub_ne_zero V, ← @vsub_ne_zero V _ _ _ _ z, vadd_vsub_assoc, vsub_self,
    vadd_vsub_assoc, ← neg_vsub_eq_vsub_rev z x, ← @neg_one_smul R, ← add_smul, ← sub_eq_add_neg]

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x z : P
hxz : x ≠ z
t : R
ht : t ∈ Set.Ioo 0 1
⊢ t • (z -ᵥ x) + 0 ≠ 0 ∧ (t - 1) • (z -ᵥ x) ≠ 0
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
h : ∃ r, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
⊢ Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w)
    ((Finset.affineCombination R s p) w₂)

Tactic:
rcases h with ⟨r, hr⟩

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
r : R
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w)
    ((Finset.affineCombination R s p) w₂)
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: case some.h₀
l : Type u_2
m : Type u_3
n✝ : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n✝
M : Matrix l m α
f : m ≃. n✝
i : l
j : n✝
fj : m
h : f.symm j = some fj
b : m
n : b ≠ fj
⊢ (M i b * if j ∈ f b then 1 else 0) = 0

Tactic:
simp [h, ← f.eq_some_iff, n.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✝⁶ : Ring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)
w : Fin (2 + 1) → R
hw : ∑ i, w i = 1
hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)
h₁' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    line[R, (Finset.affineCombination R Finset.univ t.points) (Pi.single i₁ 1),
      (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)]
h₂' :
  (Finset.affineCombination R Finset.univ t.points) w ∈ line[R, t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂]
h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)
h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)
hss : SignType.sign (w i₃) = 1
hs' : SignType.sign (∑ i, w i) = SignType.sign (w i₃)
hs : ∀ (i : Fin 3), SignType.sign (w i) = 1
⊢ w i₁ ∈ Set.Ioo 0 1

Tactic:
sign_eq_one_iff

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)
w : Fin (2 + 1) → R
hw : ∑ i, w i = 1
hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)
h₁' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    line[R, (Finset.affineCombination R Finset.univ t.points) (Pi.single i₁ 1),
      (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)]
h₂' :
  (Finset.affineCombination R Finset.univ t.points) w ∈ line[R, t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂]
h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)
h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)
hss : SignType.sign (w i₃) = 1
hs' : SignType.sign (∑ i, w i) = SignType.sign (w i₃)
hs : ∀ (i : Fin 3), 0 < w i
⊢ w i₁ ∈ Set.Ioo 0 1
Module: Mathlib.Analysis.Convex.Body

Goal state before:
pp: case inr
V : Type u_1
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup V
inst✝¹ : Module ℝ V
inst✝ : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
y : V
hy : y ∈ ↑K
hx : a • y ∈ a • ↑K
⊢ a • y ∈ b • ↑K

Tactic:
← Set.mem_inv_smul_set_iff₀ ha.ne',

Goal state after:
case inr
V : Type u_1
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup V
inst✝¹ : Module ℝ V
inst✝ : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
y : V
hy : y ∈ ↑K
hx : a • y ∈ a • ↑K
⊢ y ∈ a⁻¹ • b • ↑K
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
w x y z : P
h₁ : Wbtw R w x z
h₂ : Wbtw R x y z
⊢ Wbtw R w x y

Tactic:
rw [wbtw_comm] at *
  exact h₁.trans_left_right h₂

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
C D : PointedCone R M
⊢ dual p ↑(C ⊔ D) = dual p (↑C ∪ ↑D)

Tactic:
simp [← dual_hull]

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
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₁
z : E ⊗[ℝ] F
hz : z ∈ C₁.maxTensorProduct ↑C₂
⊢ z ∈ C₁.minTensorProduct ↑C₂

Tactic:
rw [← (equivFinsuppOfBasisLeft b).symm_apply_apply z,
    TensorProduct.equivFinsuppOfBasisLeft_symm_apply, Finsupp.sum_fintype _ _ (by simp)]

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₁
z : E ⊗[ℝ] F
hz : z ∈ C₁.maxTensorProduct ↑C₂
⊢ ∑ i, b i ⊗ₜ[ℝ] ((equivFinsuppOfBasisLeft b) z) i ∈ C₁.minTensorProduct ↑C₂
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s t : Set E
h₀ : t ∈ 𝓝 0
hc : Convex ℝ t
x : E
hx : x ∈ interior s
⊢ gaugeRescale s t x ∈ interior t

Tactic:
← gauge_lt_one_iff_mem_interior

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s t : Set E
h₀ : t ∈ 𝓝 0
hc : Convex ℝ t
x : E
hx : x ∈ interior s
⊢ gauge t (gaugeRescale s t x) < 1

case hc
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s t : Set E
h₀ : t ∈ 𝓝 0
hc : Convex ℝ t
x : E
hx : x ∈ interior s
⊢ Convex ℝ t

case hs₀
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s t : Set E
h₀ : t ∈ 𝓝 0
hc : Convex ℝ t
x : E
hx : x ∈ interior s
⊢ t ∈ 𝓝 0
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Subsingleton ι
p : ι → E
⊢ ConvexIndependent 𝕜 p

Tactic:
intro s

Goal state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
⊢ ∀ (x : ι), p x ∈ (convexHull 𝕜) (p '' s) → x ∈ s
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
⊢ ConvexIndependent 𝕜 (p ∘ ⇑f)

Tactic:
intro s

Goal state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
⊢ ∀ (x : ι'), (p ∘ ⇑f) x ∈ (convexHull 𝕜) (p ∘ ⇑f '' s) → x ∈ s
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ (convexHull 𝕜) (s ∪ t) = convexJoin 𝕜 ((convexHull 𝕜) s) ((convexHull 𝕜) t)

Tactic:
by
  rw [← convexHull_convexHull_union_left, ← convexHull_convexHull_union_right]
  exact (convex_convexHull 𝕜 s).convexHull_union (convex_convexHull 𝕜 t) hs.convexHull ht.convexHull

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

Goal state before:
pp: case inr
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
⊢ ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Bornology.IsBounded t → μ (frontier t) = 0

Tactic:
intro s

Goal state after:
case inr
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
⊢ Convex ℝ s → x ∈ interior s → Bornology.IsBounded s → μ (frontier s) = 0
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
⊢ μ (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤ ↑(r ^ d) * μ (interior s)

Tactic:
by
    refine (measure_mono <|
      hs.closure_subset_image_homothety_interior_of_one_lt hx r hr).trans_eq ?_
    rw [addHaar_image_homothety, ← NNReal.coe_pow, NNReal.abs_eq, ENNReal.ofReal_coe_nnreal]

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

Goal state before:
pp: X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
⊢ ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y

Tactic:
intro s

Goal state after:
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s✝ t : ℝ
hs : 0 ≤ s✝
ht : 0 ≤ t
h : s✝ + t = 1
x y : X
s : ℝ
⊢ ∀ {t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X), dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
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:
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.Radon

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

Tactic:
intro I

Goal state after:
ι : 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_card : finrank 𝕜 E + 1 ≤ #s
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
⊢ I ⊆ s → #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
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
⊢ ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty

Tactic:
intro I

Goal state after:
𝕜 : 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)
⊢ I ⊆ F → #I ≤ finrank 𝕜 E + 1 → (⋂₀ ↑I).Nonempty
Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
G : SimpleGraph ι
⊢ IsRelLowerSet ({s | ∃ v, s = {v}} ∪ Sym2.toFinset '' G.edgeSet) Finset.Nonempty

Tactic:
intro s

Goal state after:
ι : Type u_1
inst✝ : DecidableEq ι
G : SimpleGraph ι
s : Finset ι
⊢ s ∈ {s | ∃ v, s = {v}} ∪ Sym2.toFinset '' G.edgeSet →
    s.Nonempty ∧ ∀ ⦃b : Finset ι⦄, b ⊆ s → b.Nonempty → b ∈ {s | ∃ v, s = {v}} ∪ Sym2.toFinset '' G.edgeSet
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: case inr.hst
ι : 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 : ι
⊢ ∀ (u : Finset ι), (F i0 ∩ ⋂ i ∈ u, F i).Nonempty

Tactic:
intro I

Goal state after:
case inr.hst
ι : 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 : Finset ι
⊢ (F i0 ∩ ⋂ i ∈ I, F i).Nonempty
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: ι : 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_card : ↑(finrank 𝕜 E) + 1 ≤ ENat.card ι
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
⊢ ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty

Tactic:
intro I

Goal state after:
ι : 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_card : ↑(finrank 𝕜 E) + 1 ≤ ENat.card ι
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
I : Finset ι
⊢ #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
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
⊢ ∀ (G : Finset (Set E)), ↑G ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty

Tactic:
intro I

Goal state after:
𝕜 : 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)
⊢ ↑I ⊆ F → #I ≤ finrank 𝕜 E + 1 → (⋂₀ ↑I).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hne : v ≠ w
he : s(v, w) ∈ G.edgeSet
⊢ G.Adj v w

Tactic:
mem_edgeSet

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
hne : v ≠ w
he : G.Adj v w
⊢ G.Adj v w
Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow

Goal state before:
pp: p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • (fun x ↦ x ^ p) x + b • (fun x ↦ x ^ p) y < (fun x ↦ x ^ p) (a • x + b • y)

Tactic:
let x' : ℝ≥0 := .mk x hx

Goal state after:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := NNReal.mk x hx
⊢ a • (fun x ↦ x ^ p) x + b • (fun x ↦ x ^ p) y < (fun x ↦ x ^ p) (a • x + b • y)
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ G = fromEdgeSet s ∧ Disjoint s Sym2.diagSet → G.edgeSet = s

Tactic:
by rintro ⟨rfl, hs⟩; simp [hs]

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

Goal state before:
pp: V : Type u
G H : SimpleGraph V
⊢ (∀ (v : V) ⦃a : V⦄, G.Adj v a → ¬H.Adj v a) ↔ ∀ (x y : V), s(x, y) ∈ G.edgeSet → s(x, y) ∉ H.edgeSet

Tactic:
mem_edgeSet

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
⊢ s(v, w) ∈ G.incidenceSet v ↔ G.Adj v w

Tactic:
by
  simp [incidenceSet]

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

Goal state before:
pp: V : Type u
G H : SimpleGraph V
⊢ (∀ (u v : V) ⦃a : V⦄, G.Adj u a ∧ G.Adj v a → ¬(H.Adj u a ∧ H.Adj v a)) ↔
    ∀ (x y : V), s(x, y) ∈ G.edgeSet → s(x, y) ∉ H.edgeSet

Tactic:
mem_edgeSet

Goal state after:
V : Type u
G H : SimpleGraph V
⊢ (∀ (u v : V) ⦃a : V⦄, G.Adj u a ∧ G.Adj v a → ¬(H.Adj u a ∧ H.Adj v a)) ↔ ∀ (x y : V), G.Adj x y → ¬H.Adj x y