mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: u : ℝˣ
z : ℍ
⊢ denom ((GeneralLinearGroup.scalar (Fin 2)) u) ↑z = ↑↑u

Tactic:
simp [denom]

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
⊢ M k k ^ 1 • det 1 * ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det =
    M k k * ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det

Tactic:
pow_one,

Goal state after:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
⊢ M k k • det 1 * ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det =
    M k k * ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
⊢ dist c (inversion c R x) = R ^ 2 / dist c x

Tactic:
rw [dist_comm c, dist_comm c, dist_inversion_center]

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist z.im (w.im * ((z.im / w.im + (z.im / w.im)⁻¹) / 2)) = w.im * |(z.im / w.im - (z.im / w.im)⁻¹) / 2|

pp: z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ (↑z).re = (↑(w.center |log (z.im / w.im)|)).re

Tactic:
inv_div

Goal state after:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist z.im (w.im * ((z.im / w.im + w.im / z.im) / 2)) = w.im * |(z.im / w.im - w.im / z.im) / 2|

z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ (↑z).re = (↑(w.center |log (z.im / w.im)|)).re
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
s : Set α
hs : s ∈ ↑A
⊢ s ∈ ↑B

Tactic:
rw [connectedComponent_eq_iInter_isClopen, Set.mem_iInter] at hB

Goal state after:
α : Type u
A B : Ultrafilter α
hB : ∀ (i : { s // IsClopen s ∧ A ∈ s }), B ∈ ↑i
s : Set α
hs : s ∈ ↑A
⊢ s ∈ ↑B
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h₁ : IsClosed[inst✝] s
h₂ : IsCompact s
⊢ (some '' s)ᶜ ∩ {∞}ᶜ ⊆ some '' sᶜ

Tactic:
simp [compl_image_coe, ← sdiff_eq]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case coe
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : T1Space X
x✝ : X
⊢ IsClosed[instTopologicalSpace] {↑x✝}

Tactic:
rw [← image_singleton, isClosed_image_coe]
      exact ⟨isClosed_singleton, isCompact_singleton⟩

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
a₀ : E
⊢ ℝ → ℝ

Tactic:
by_cases h : a = ⊤
  · exact circleAverage (log⁺ ‖f ·‖) 0
  · exact circleAverage (log⁺ ‖f · - a.untop₀‖⁻¹) 0

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case hf₂
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x‖⁻¹) 0 R

Tactic:
simp_rw [← norm_inv]
    apply h₁f.inv.meromorphicOn.circleIntegrable_posLog_norm

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: case h₂f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
⊢ θ ∈ sphere 0 |r| → |(fun x ↦ log⁺ ‖f x‖) - fun x ↦ log⁺ ‖f x - a₀‖| θ ≤ log⁺ ‖a₀‖ + log 2

Tactic:
hθ

Goal state after:
case h₂f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : θ ∈ sphere 0 |r|
⊢ |(fun x ↦ log⁺ ‖f x‖) - fun x ↦ log⁺ ‖f x - a₀‖| θ ≤ log⁺ ‖a₀‖ + log 2
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mpr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = ↑l * (y - x)
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
xy : x ≤ y
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))

Tactic:
rw [← h.2 xs ys, variationOnFromTo.eq_of_le f s xy, ENNReal.ofReal_toReal (h.1 x y xs ys)]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
e : E
n : ℤ
⊢ logCounting (single e n) =O[atTop] log

Tactic:
by
  have h₁ : logCounting (single e n) =ᶠ[atTop] (n * log · - n * log ‖e‖) := by
    filter_upwards [eventually_ge_atTop ‖e‖] with r hr
    rw [logCounting_single_eq_log_sub_const hr]
    ring
  have hb : (n * log ·) =O[atTop] Real.log := isBigO_const_mul_self (n : ℝ) log atTop
  exact (hb.sub isLittleO_const_log_atTop.isBigO).congr' h₁.symm EventuallyEq.rfl

Goal state after:
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z ↦ ↑z) s' ≠ univ → #s' < #((image (fun z ↦ ↑z) s').biUnion t)
he : s'.Nonempty
ha' : #s' < #(s'.biUnion fun x_1 ↦ t ↑x_1)
hb : a ∈ s'.biUnion fun x_1 ↦ t ↑x_1
⊢ #s' ≤ #((s'.biUnion fun x' ↦ t ↑x').erase a)

Tactic:
rw [card_erase_of_mem hb]
      exact Nat.le_sub_one_of_lt ha'

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
L : StrongDual 𝕜 (E × 𝕜)
b : ℝ
hLb : re (L (x, ↑a)) < b ∧ ∀ b_1 ∈ {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}, b < re (L b_1)
u : E →L[𝕜] 𝕜 := L ∘SL inl 𝕜 E 𝕜
c : ℝ := (re (L (0, 1)))⁻¹
z : ↑s
hv : ∀ (v : 𝕜), v * L (0, 1) = L (0, v)
w : E
h : w ∈ s
hw :
  re (((L ∘SL inl 𝕜 E 𝕜).coprod (L ∘SL inr 𝕜 E 𝕜)) (x, ↑a)) <
    re (((L ∘SL inl 𝕜 E 𝕜).coprod (L ∘SL inr 𝕜 E 𝕜)) (w, ↑(φ w)))
⊢ re (L (x, 0)) + re (L (0, 1)) * a < re (L (w, 0)) + re (L (0, 1)) * φ w

Tactic:
simpa [-coprod_comp_inl_inr, ← hv (ofReal a), ← hv (ofReal (φ w)), mul_comm a,
        mul_comm (φ w)] using hw

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
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 • (z -ᵥ x) + (x -ᵥ z) ≠ 0

Tactic:
← neg_vsub_eq_vsub_rev z x,

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 • (z -ᵥ x) + -(z -ᵥ x) ≠ 0
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕'.Nonempty
⊢ ∃ l c,
    (∀ (i : ℕ), s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i) ≤ s.domRestrict φ) ∧
      ⨆ i, s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i) = s.domRestrict φ

pp: case neg
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕' = ∅
⊢ ∃ l c,
    (∀ (i : ℕ), s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i) ≤ s.domRestrict φ) ∧
      ⨆ i, s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i) = s.domRestrict φ

Tactic:
· obtain ⟨f, hf⟩ := h𝓕'.1.exists_eq_range he
    have (i : ℕ) : ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f i = s.domRestrict (re ∘ l) + const s c := by simp_all
    choose l c hlc using this
    refine ⟨l, c, fun i => (hlc i) ▸ (h𝓕'.2.2 (f i) (hf ▸ mem_range_self i)).1, ?_⟩
    calc
    _ = ⨆ i, f i := by congr with i x; exact congrFun (hlc i).symm x
    _ = _ := by rw [← sSup_range, ← hf, h𝓕'.2.1]

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕' = ∅
⊢ ∃ l c,
    (∀ (i : ℕ), s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i) ≤ s.domRestrict φ) ∧
      ⨆ i, s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i) = s.domRestrict φ
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

Goal state before:
pp: R✝ : Type u_1
n✝ : Type u_2
inst✝⁹ : Fintype n✝
inst✝⁸ : DecidableEq n✝
inst✝⁷ : Semiring R✝
inst✝⁶ : PartialOrder R✝
inst✝⁵ : IsOrderedRing R✝
M✝ : Matrix n✝ n✝ R✝
x : n✝ → R✝
R : Type u_3
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M N : Matrix n n R
hM : M ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1}
⊢ M * N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1}

Tactic:
refine Set.mem_sep ?_ ?_

Goal state after:
case refine_1
R✝ : Type u_1
n✝ : Type u_2
inst✝⁹ : Fintype n✝
inst✝⁸ : DecidableEq n✝
inst✝⁷ : Semiring R✝
inst✝⁶ : PartialOrder R✝
inst✝⁵ : IsOrderedRing R✝
M✝ : Matrix n✝ n✝ R✝
x : n✝ → R✝
R : Type u_3
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M N : Matrix n n R
hM : M ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1}
⊢ M * N ∈ fun M ↦ ∀ (i j : n), 0 ≤ M i j

case refine_2
R✝ : Type u_1
n✝ : Type u_2
inst✝⁹ : Fintype n✝
inst✝⁸ : DecidableEq n✝
inst✝⁷ : Semiring R✝
inst✝⁶ : PartialOrder R✝
inst✝⁵ : IsOrderedRing R✝
M✝ : Matrix n✝ n✝ R✝
x : n✝ → R✝
R : Type u_3
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M N : Matrix n n R
hM : M ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1}
⊢ 1 ᵥ* (M * N) = 1
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : Matrix n n R
hx : x ∈ ↑(colStochastic R n)
y : Matrix n n R
hy : y ∈ ↑(colStochastic R n)
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
h : a + b = 1
⊢ a • x + b • y ∈ ↑(colStochastic R n)

Tactic:
simp only [SetLike.mem_coe, mem_colStochastic_iff_sum] at hx hy ⊢

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : Matrix n n R
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
h : a + b = 1
hx : (∀ (i j : n), 0 ≤ x i j) ∧ ∀ (j : n), ∑ i, x i j = 1
hy : (∀ (i j : n), 0 ≤ y i j) ∧ ∀ (j : n), ∑ i, y i j = 1
⊢ (∀ (i j : n), 0 ≤ (a • x + b • y) i j) ∧ ∀ (j : n), ∑ i, (a • x + b • y) i j = 1
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
x : E
hx : ¬gauge t x = 0
⊢ gauge t (gaugeRescale s t x) ≤ gauge s x

Tactic:
exact (gauge_gaugeRescale' s hx).le

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ (convexHull 𝕜) ↑t
this : p x ∈ t
⊢ p x ∈ ↑t

Tactic:
← mem_coe

Goal state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ (convexHull 𝕜) ↑t
this : p x ∈ ↑t
⊢ p x ∈ ↑t
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: X : Type u_2
K : Type u_8
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : IsDomain K
w : StdSimplex K X
x : X
hx : ∃ x_1 ∈ {x}, w.weights x_1 ≠ 0
⊢ w.restrict {x} hx = single x

Tactic:
simp only [← support_weights_eq_singleton, support_weights_restrict, Set.mem_singleton_iff]

Goal state after:
X : Type u_2
K : Type u_8
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : IsDomain K
w : StdSimplex K X
x : X
hx : ∃ x_1 ∈ {x}, w.weights x_1 ≠ 0
⊢ {x_1 ∈ w.weights.support | x_1 = x} = {x}
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: 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
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄, ↑t ⊆ s → t = w.weights.support → sConvexComb w ∈ s
w : StdSimplex K X
hw : ↑(Finset.cons x t hx) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : w.weights x ≠ 0
hwx' : ∃ y, y ≠ x ∧ w.weights y ≠ 0
⊢ ↑t ⊆ s

Tactic:
← hw,

Goal state after:
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
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄, ↑t ⊆ s → t = w.weights.support → sConvexComb w ∈ s
w : StdSimplex K X
hw : ↑(Finset.cons x t hx) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : w.weights x ≠ 0
hwx' : ∃ y, y ≠ x ∧ w.weights y ≠ 0
⊢ ↑t ⊆ ↑(Finset.cons x t hx)
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ dist (convexCombPair (↑i) (1 - ↑i) ⋯ ⋯ ⋯ x.1 x.2) (convexCombPair (↑i) (1 - ↑i) ⋯ ⋯ ⋯ y.1 y.2) ≤ dist x y

Tactic:
dist_convexCombPair_convexCombPair_le,

Goal state after:
case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ ↑i * dist x.1 y.1 + (1 - ↑i) * dist x.2 y.2 ≤ dist x y
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

Goal state after:
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
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
hJ_fin : Fintype ↑J
J' : Finset (Set E) := J.toFinset
⊢ (⋂₀ J).Nonempty

Tactic:
rw [← coe_toFinset J]

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)
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
hJ_fin : Fintype ↑J
J' : Finset (Set E) := J.toFinset
⊢ (⋂₀ ↑J.toFinset).Nonempty
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
⊢ x ∉ s → y ∉ s → ((y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))

Tactic:
rintro _ hy

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
a✝ : x ∉ s
hy : y ∉ s
⊢ (y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
Module: Mathlib.Analysis.Convex.StrictCombination

Goal state before:
pp: case e_6.inl
V : Type u_2
P : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : ∑ i, w i = 1
hw01 : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
hij : ∀ (j : Fin (n + 1)), i ≠ j → w j = 0
⊢ w i = 1

Tactic:
← hw,

Goal state after:
case e_6.inl
V : Type u_2
P : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : ∑ i, w i = 1
hw01 : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
hij : ∀ (j : Fin (n + 1)), i ≠ j → w j = 0
⊢ w i = ∑ i, w i
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 : UniformConvexOn s φ f
⊢ UniformConcaveOn s φ (-f)

Tactic:
refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ le_of_neg_le_neg ?_⟩

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ -(-f) (a • x + b • y) ≤ -(a • (-f) x + b • (-f) y + a * b * φ ‖x - 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
⊢ UniformConvexOn s φ (-f)

Tactic:
refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ le_of_neg_le_neg ?_⟩

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ -(a • (-f) x + b • (-f) y - a * b * φ ‖x - y‖) ≤ -(-f) (a • x + b • y)
Module: Mathlib.Analysis.Convex.Visible

Goal state before:
pp: case refine_2
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝¹ : 0 < w i
hwi✝ : w i < 1
ε : 𝕜
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
hε₁ : ε < 1
this : 0 < 1 - ε
hwi : 0 < 1 - w i
⊢ (lineMap ((lineMap x (a i)) ε) (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j))
      ((1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1)) =
    (lineMap x (∑ j ∈ t, w j • a j)) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹))

Tactic:
have :
        w i • a i + (1 - w i) • ∑ j ∈ t.erase i, (w j / (1 - w i)) • a j = ∑ j ∈ t, w j • a j := by
        rw [smul_sum]
        simp_rw [smul_smul, mul_div_cancel₀ _ hwi.ne']
        exact add_sum_erase _ (fun i ↦ w i • a i) hi

Goal state after:
case refine_2
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝¹ : 0 < w i
hwi✝ : w i < 1
ε : 𝕜
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
hε₁ : ε < 1
this✝ : 0 < 1 - ε
hwi : 0 < 1 - w i
this : w i • a i + (1 - w i) • ∑ j ∈ t.erase i, (w j / (1 - w i)) • a j = ∑ j ∈ t, w j • a j
⊢ (lineMap ((lineMap x (a i)) ε) (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j))
      ((1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1)) =
    (lineMap x (∑ j ∈ t, w j • a j)) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹))