mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
D' : locallyFinsupp E ℤ := ∑ z ∈ t, single z 1
hD' : D' = ∑ z ∈ t, single z 1
hle : D' ≤ D
R₀ : ℝ
hR₀ : ∀ z ∈ t, ‖z‖ ≤ R₀
K : ℝ := ∑ z ∈ t, log ‖z‖
hK : K = ∑ z ∈ t, log ‖z‖
hEq : ∀ᶠ (r : ℝ) in atTop, logCounting D' r = ↑N * log r - K
⊢ ∀ᶠ (r : ℝ) in atTop, (↑N - C) * log r ≤ K

Tactic:
filter_upwards [hEq, eventually_ge_atTop (1 : ℝ), hC] with r hr₁ hr₂ hr₃

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
D' : locallyFinsupp E ℤ := ∑ z ∈ t, single z 1
hD' : D' = ∑ z ∈ t, single z 1
hle : D' ≤ D
R₀ : ℝ
hR₀ : ∀ z ∈ t, ‖z‖ ≤ R₀
K : ℝ := ∑ z ∈ t, log ‖z‖
hK : K = ∑ z ∈ t, log ‖z‖
hEq : ∀ᶠ (r : ℝ) in atTop, logCounting D' r = ↑N * log r - K
r : ℝ
hr₁ : logCounting D' r = ↑N * log r - K
hr₂ : 1 ≤ r
hr₃ : ‖logCounting D r‖ ≤ C * ‖log r‖
⊢ (↑N - C) * log r ≤ K
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
⊢ logCounting f ⊤ =O[atTop] log ↔ (MeromorphicOn.divisor f univ)⁻.support.Finite

Tactic:
rw [logCounting_top]

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
⊢ locallyFinsuppWithin.logCounting (MeromorphicOn.divisor f univ)⁻ =O[atTop] log ↔
    (MeromorphicOn.divisor f univ)⁻.support.Finite
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
x✝ : ℝ
⊢ φ 0 = 0

Tactic:
have hm : 0 ∈ φ '' Icc 0 s := by simp only [φst, ht, mem_Icc, le_refl, and_self]

Goal state after:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
x✝ : ℝ
hm : 0 ∈ φ '' Icc 0 s
⊢ φ 0 = 0
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
l : List P
f : P ≃ᵃ[R] P'
⊢ List.Wbtw R (map (⇑f) l) ↔ List.Wbtw R l

Tactic:
by
  have hf : Function.Injective f.toAffineMap := f.injective
  apply hf.list_wbtw_map_iff

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

Goal state before:
pp: α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z ↦ ↑z) s')
this : #s' = #(s ∪ image (fun z ↦ ↑z) s') - #s
⊢ #(s ∪ image (fun z ↦ ↑z) s') - #s ≤ #(s'.biUnion fun x' ↦ t ↑x' \ s.biUnion t)

Tactic:
hus

Goal state after:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z ↦ ↑z) s')
this : #s' = #(s ∪ image (fun z ↦ ↑z) s') - #s
⊢ #(s ∪ image (fun z ↦ ↑z) s') - #(s.biUnion t) ≤ #(s'.biUnion fun x' ↦ t ↑x' \ s.biUnion t)
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case refine_2
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
l : List P
hl : l ≠ []
h : List.Sbtw R l
⊢ ∃ l', l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)

Tactic:
rw [List.Sbtw, ← exists_map_eq_of_sorted_nonempty_iff_wbtw hl] at h

Goal state after:
case refine_2
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
l : List P
hl : l ≠ []
h : (∃ l', l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l) ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
⊢ ∃ l', l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
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 φ
hs : s = ∅
⊢ ∃ 𝓕',
    𝓕'.Countable ∧
      sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c

Tactic:
· use ∅; simp [domRestrict_def]; grind

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg : F.eventualRange j = range ⇑(ConcreteCategory.hom (F.map g))
x : F.obj k
hx : (ConcreteCategory.hom (F.map (g ≫ f))) x ∈ F.eventualRange i
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (F.map g)) x) = (ConcreteCategory.hom (F.map (g ≫ f))) x

Tactic:
by rw [map_comp, comp_apply]

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : i ⟶ j
h : ∀ ⦃k : J⦄ (g : k ⟶ i), range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map (g ≫ f)))
j' : J
f' : j' ⟶ j
k : J
g : k ⟶ i
g' : k ⟶ j'
he : g ≫ f = g' ≫ f'
⊢ range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map f'))

Tactic:
refine (h g).trans ?_

Goal state after:
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : i ⟶ j
h : ∀ ⦃k : J⦄ (g : k ⟶ i), range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map (g ≫ f)))
j' : J
f' : j' ⟶ j
k : J
g : k ⟶ i
g' : k ⟶ j'
he : g ≫ f = g' ≫ f'
⊢ range ⇑(ConcreteCategory.hom (F.map (g ≫ f))) ⊆ range ⇑(ConcreteCategory.hom (F.map f'))
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
⊢ (∀ (j : J), ∃ i f, F.eventualRange j = range ⇑(ConcreteCategory.hom (F.map f))) ↔
    ∀ (j : J),
      ∃ i f,
        ∀ ⦃k : J⦄ (g : k ⟶ i), range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map (g ≫ f)))

Tactic:
eventualRange_eq_iff

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

Goal state before:
pp: ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
ι' : (Finset ι)ᵒᵖ
⊢ Finite ((hallMatchingsFunctor t).obj ι')

Tactic:
rw [hallMatchingsFunctor]

Goal state after:
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
ι' : (Finset ι)ᵒᵖ
⊢ Finite
    ({ obj := fun ι' ↦ ↑(hallMatchingsOn t (Opposite.unop ι')), map := fun {x x_1} g ↦ ↾hallMatchingsOn.restrict t ⋯,
          map_id := ⋯, map_comp := ⋯ }.obj
      ι')
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α ≃. β
g : β ≃. γ
a : α
⊢ (f.trans g) a = none ↔ ∀ (b : β) (c : γ), ¬b ∈ f a ∨ ¬c ∈ g b

Tactic:
simp only [eq_none_iff_forall_not_mem, mem_trans, imp_iff_not_or.symm]

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
g : β ≃. γ
a : α
⊢ (∀ (a_1 : γ), ¬∃ b, b ∈ f a ∧ a_1 ∈ g b) ↔ ∀ (b : β) (c : γ), b ∈ f a → ¬c ∈ g b
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: case refine_2
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range ⇑(ConcreteCategory.hom (F.map f₂))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' s
this : (ConcreteCategory.hom (F.map f₂)) x ∈ F.eventualRange j₁
y : F.obj j₃
hy : y ∈ F.eventualRange j₃
h₃ : (ConcreteCategory.hom (F.map (f₃ ≫ f₂))) y = (ConcreteCategory.hom (F.map f₂)) x
⊢ ↑((ConcreteCategory.hom ((F.toPreimages s).map (f₃ ≫ f₂ ≫ f₁))) ⟨y, ⋯⟩) =
    ↑((ConcreteCategory.hom ((F.toPreimages s).map (f₂ ≫ f₁))) ⟨x, hx⟩)

Tactic:
· simp only [toPreimages_obj, toPreimages_map, ConcreteCategory.hom_ofHom,
        TypeCat.Fun.coe_mk, MapsTo.val_restrict_apply]
      rw [← Category.assoc, map_comp, comp_apply, h₃, map_comp, comp_apply]

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

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 ∈ ↑(doublyStochastic R n)
y : Matrix n n R
hy : y ∈ ↑(doublyStochastic R n)
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
h : a + b = 1
⊢ a • x + b • y ∈ ↑(doublyStochastic R n)

Tactic:
simp only [SetLike.mem_coe, mem_doublyStochastic_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) ∧ (∀ (i : n), ∑ j, x i j = 1) ∧ ∀ (j : n), ∑ i, x i j = 1
hy : (∀ (i j : n), 0 ≤ y i j) ∧ (∀ (i : n), ∑ j, y i j = 1) ∧ ∀ (j : n), ∑ i, y i j = 1
⊢ (∀ (i j : n), 0 ≤ (a • x + b • y) i j) ∧
    (∀ (i : n), ∑ j, (a • x + b • y) i j = 1) ∧ ∀ (j : n), ∑ i, (a • x + b • y) i j = 1
Module: Mathlib.Analysis.Convex.Caratheodory

Goal state before:
pp: 𝕜 : Type u_1
E : Type u
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
⊢ ∑ x ∈ t, f x - ∑ x ∈ t, f i₀ / g i₀ * g x = 1

Tactic:
fsum,

Goal state after:
𝕜 : Type u_1
E : Type u
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
⊢ 1 - ∑ x ∈ t, f i₀ / g i₀ * g x = 1
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : PartialOrder R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : ClosedIciTopology R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
hp : ∀ (x : M), Continuous ⇑(p x)
⊢ IsClosed ↑(dual p s)

Tactic:
rw [← s.biUnion_of_singleton]
  simp_rw [dual_iUnion, Submodule.coe_iInf, dual_singleton]
  exact isClosed_biInter fun x hx ↦ isClosed_Ici.preimage <| hp _

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

Goal state before:
pp: case inr.inr.inl
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 : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : 0 < ty
hz0 : tz < 0
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

Tactic:
refine Or.inr (Or.inr (wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg _ _ hz0.le hy0.le))

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

Goal state before:
pp: case mem
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
s : Set M
x : N
hx : x ∈ dual p s
y _y : M
h : _y ∈ s
⊢ 0 ≤ (p _y) x

Tactic:
exact hx h

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ : 0 ∈ interior ((convexHull ℝ) (range ⇑b))
hb₂ : (convexHull ℝ) (range ⇑b) ⊆ V
u : Finset E
hu₁ : ↑u ⊆ s
hu₃ : s ⊆ ⋃ i ∈ ↑u, interior ((convexHull ℝ) (range ⇑b)) + {i}
⊢ s ⊆ interior ((convexHull ℝ) (⇑b '' univ + ↑u))

Tactic:
Set.image_univ,

Goal state after:
case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ : 0 ∈ interior ((convexHull ℝ) (range ⇑b))
hb₂ : (convexHull ℝ) (range ⇑b) ⊆ V
u : Finset E
hu₁ : ↑u ⊆ s
hu₃ : s ⊆ ⋃ i ∈ ↑u, interior ((convexHull ℝ) (range ⇑b)) + {i}
⊢ s ⊆ interior ((convexHull ℝ) (range ⇑b + ↑u))
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: case inl
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
hs : Convex ℝ s
hs₀ : s ∈ 𝓝 0
ht : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
hta : Absorbent ℝ t
⊢ Tendsto (gaugeRescale s t) (𝓝 0) (comap (gauge t) (𝓝 0))

Tactic:
simp only [tendsto_comap_iff, Function.comp_def, gauge_gaugeRescale _ hta htb]

Goal state after:
case inl
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
hs : Convex ℝ s
hs₀ : s ∈ 𝓝 0
ht : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
hta : Absorbent ℝ t
⊢ Tendsto (fun x ↦ gauge s x) (𝓝 0) (𝓝 0)
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ : 0 ∈ interior ((convexHull ℝ) (range ⇑b))
hb₂ : (convexHull ℝ) (range ⇑b) ⊆ V
u : Finset E
hu₁ : ↑u ⊆ s
hu₃ : s ⊆ ⋃ i ∈ ↑u, interior ((convexHull ℝ) (range ⇑b)) + {i}
⊢ (convexHull ℝ) (⇑b '' univ + ↑u) ⊆ t

Tactic:
Set.image_univ,

Goal state after:
case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ : 0 ∈ interior ((convexHull ℝ) (range ⇑b))
hb₂ : (convexHull ℝ) (range ⇑b) ⊆ V
u : Finset E
hu₁ : ↑u ⊆ s
hu₃ : s ⊆ ⋃ i ∈ ↑u, interior ((convexHull ℝ) (range ⇑b)) + {i}
⊢ (convexHull ℝ) (range ⇑b + ↑u) ⊆ t
Module: Mathlib.Analysis.Convex.KreinMilman

Goal state before:
pp: E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun x ↦ x ∈ S) t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyx : ¬y = x
l : StrongDual ℝ E
hyB : y ∈ {z | z ∈ t ∧ ∀ w ∈ t, l w ≤ l z}
hl : l y < l x
z : E
hzt : z ∈ t
hz : IsMaxOn (⇑l) t z
h : IsExposed ℝ t {z | z ∈ t ∧ ∀ w ∈ t, l w ≤ l z}
⊢ False

Tactic:
exact hl.not_ge (hyB.2 x hxt)

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

Goal state before:
pp: case inr
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x1 x2 ↦ x1 ⊆ x2) F
hFnemp : F.Nonempty
⊢ (⋂₀ F).Nonempty

Tactic:
have : Nonempty (↥F) := hFnemp.to_subtype

Goal state after:
case inr
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x1 x2 ↦ x1 ⊆ x2) F
hFnemp : F.Nonempty
this : Nonempty ↑F
⊢ (⋂₀ F).Nonempty
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Ici y) f
hf_cont : ContinuousWithinAt f (Ici y) y
x : ℝ
hx : x ∈ Ici y
⊢ ContinuousWithinAt f (Ici y) x

Tactic:
rcases eq_or_lt_of_le (α := ℝ) hx with rfl | hxy

Goal state after:
case inl
f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Ici y) f
hf_cont : ContinuousWithinAt f (Ici y) y
hx : y ∈ Ici y
⊢ ContinuousWithinAt f (Ici y) y

case inr
f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Ici y) f
hf_cont : ContinuousWithinAt f (Ici y) y
x : ℝ
hx : x ∈ Ici y
hxy : y < x
⊢ ContinuousWithinAt f (Ici y) x
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Iic y) f
hf_cont : ContinuousWithinAt f (Iic y) y
x : ℝ
hx : x ∈ Iic y
⊢ ContinuousWithinAt f (Iic y) x

Tactic:
rcases eq_or_lt_of_le (α := ℝ) hx with rfl | hxy

Goal state after:
case inl
f : ℝ → ℝ
x : ℝ
hf_cvx : ConvexOn ℝ (Iic x) f
hf_cont : ContinuousWithinAt f (Iic x) x
hx : x ∈ Iic x
⊢ ContinuousWithinAt f (Iic x) x

case inr
f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Iic y) f
hf_cont : ContinuousWithinAt f (Iic y) y
x : ℝ
hx : x ∈ Iic y
hxy : x < y
⊢ ContinuousWithinAt f (Iic y) 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 X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
⊢ ↑u ⊆ s

Tactic:
hus

Goal state after:
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 X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
⊢ s ⊆ s
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
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : ∑ e ∈ s, w e • f e = 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
⊢ ∃ I, ((convexHull 𝕜) (f '' I) ∩ (convexHull 𝕜) (f '' Iᶜ)).Nonempty

Tactic:
have hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0 := by
    simpa only [h_wsum, not_lt] using sum_filter_add_sum_filter_not s (fun i ↦ w i < 0) w

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
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : ∑ e ∈ s, w e • f e = 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0
⊢ ∃ I, ((convexHull 𝕜) (f '' I) ∩ (convexHull 𝕜) (f '' Iᶜ)).Nonempty
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
this : dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) ≤ |s - s'| * dist x y
⊢ |t - t'| = |s - s'|

Tactic:
rw [eq_sub_iff_add_eq.mpr h, eq_sub_iff_add_eq.mpr h']

Goal state after:
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
this : dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) ≤ |s - s'| * dist x y
⊢ |t - t'| = |1 - t - (1 - t')|
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
⊢ ∀ (a : ↑(Set.Icc 0 1)), LipschitzWith 1 fun y ↦ convexCombPair (↑(a, y).1) (1 - ↑(a, y).1) ⋯ ⋯ ⋯ (a, y).2.1 (a, y).2.2

pp: case hb
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
⊢ ∀ (b : X × X), Continuous fun x ↦ convexCombPair (↑(x, b).1) (1 - ↑(x, b).1) ⋯ ⋯ ⋯ (x, b).2.1 (x, b).2.2

Tactic:
· intro i x y
    simp only [← coe_nnreal_ennreal_nndist, ENNReal.coe_one, one_mul, ENNReal.coe_le_coe,
      NNReal.toReal_le, coe_nndist]
    grw [dist_convexCombPair_convexCombPair_le, Prod.dist_eq]
    nth_grw 1 [le_max_left (dist x.1 y.1) (dist x.2 y.2)]
    swap; · simpa using i.prop.left
    nth_grw 2 [le_max_right (dist x.1 y.1) (dist x.2 y.2)]
    swap; · simpa using i.prop.right
    rw [← add_mul, add_sub_cancel, one_mul]

Goal state after:
case hb
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
⊢ ∀ (b : X × X), Continuous fun x ↦ convexCombPair (↑(x, b).1) (1 - ↑(x, b).1) ⋯ ⋯ ⋯ (x, b).2.1 (x, b).2.2
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x y : M
⊢ convexCombPair a b ha hb hab x y = a • x + b • y

Tactic:
classical simp [convexCombPair, sConvexComb_eq_sum, Finsupp.sum_add_index, add_smul]

Goal state after: