mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case refine_1
X : Type u_1
Y✝ : Type u_2
inst✝⁴ : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst✝³ : DiscreteTopology X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : Infinite X
f : C(OnePoint X, Y)
x : OnePoint X
⊢ ((fun f ↦
          {
            toFun := fun x ↦
              match x with
              | none => Classical.choose ⋯
              | Option.some x => ↑f x,
            continuous_toFun := ⋯ })
        ((fun f ↦ ⟨fun x ↦ f ↑x, ⋯⟩) f))
      ∞ =
    f ∞

pp: case refine_2
X : Type u_1
Y✝ : Type u_2
inst✝⁴ : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst✝³ : DiscreteTopology X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : Infinite X
f : C(OnePoint X, Y)
x : OnePoint X
⊢ ∀ (x : X),
    ((fun f ↦
            {
              toFun := fun x ↦
                match x with
                | none => Classical.choose ⋯
                | Option.some x => ↑f x,
              continuous_toFun := ⋯ })
          ((fun f ↦ ⟨fun x ↦ f ↑x, ⋯⟩) f))
        ↑x =
      f ↑x

Tactic:
· refine tendsto_nhds_unique ?_ (continuous_iff_from_discrete _ |>.mp <| map_continuous f)
      let f' : { f : X → Y // ∃ L, Tendsto (fun x : X ↦ f x) cofinite (𝓝 L) } :=
        ⟨fun x ↦ f x, ⟨f ∞, continuous_iff_from_discrete f |>.mp <| map_continuous f⟩⟩
      exact Classical.choose_spec f'.property

Goal state after:
case refine_2
X : Type u_1
Y✝ : Type u_2
inst✝⁴ : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst✝³ : DiscreteTopology X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : Infinite X
f : C(OnePoint X, Y)
x : OnePoint X
⊢ ∀ (x : X),
    ((fun f ↦
            {
              toFun := fun x ↦
                match x with
                | none => Classical.choose ⋯
                | Option.some x => ↑f x,
              continuous_toFun := ⋯ })
          ((fun f ↦ ⟨fun x ↦ f ↑x, ⋯⟩) f))
        ↑x =
      f ↑x
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (OnePoint.map f) ↔
    Continuous[inst✝¹, inst✝] f ∧ Tendsto f (coclosedCompact X) (coclosedCompact Y)

Tactic:
continuous_iff,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Tendsto (fun x ↦ OnePoint.map f ↑x) (coclosedCompact X) (𝓝 (OnePoint.map f ∞)) ∧
      Continuous[inst✝¹, instTopologicalSpace] fun x ↦ OnePoint.map f ↑x) ↔
    Continuous[inst✝¹, inst✝] f ∧ Tendsto f (coclosedCompact X) (coclosedCompact Y)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
s : Set (OnePoint X)
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
⊢ ∀ t ∈ 𝓝 y, ∃ i, IsCompact i ∧ MapsTo f iᶜ t

Tactic:
intro N

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
s : Set (OnePoint X)
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
N : Set Y
⊢ N ∈ 𝓝 y → ∃ i, IsCompact i ∧ MapsTo f iᶜ N
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✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
this : Tendsto f (coclosedCompact X) (𝓝 y)
p : X
⊢ (fun q ↦ if hq : q = y then ∞ else ↑(Exists.choose ⋯)) ((fun p ↦ p.elim y f) ↑p) = ↑p

Tactic:
| coe p =>

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

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
h_int_Bound : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) μ
β : ℝ
h_int_nonneg : 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ
h_bound_nonneg : 0 ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
⊢ ∀ (x : ℝ), 0 x ≤ (fun α ↦ (cartanKernel f R α β)⁺) x

Tactic:
by simp [posPart]

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

Goal state before:
pp: case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
a : ℝ
ha : a ∈ Ioi ‖e‖
b : ℝ
hb : b ∈ Ioi ‖e‖
hab : a < b
⊢ logCounting (single e 1) a < logCounting (single e 1) b

Tactic:
mem_Ioi

Goal state after:
case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
a : ℝ
ha : ‖e‖ < a
b : ℝ
hb : ‖e‖ < b
hab : a < b
⊢ logCounting (single e 1) a < logCounting (single e 1) b
Module: Mathlib.Topology.Semicontinuity.Lindelof

Goal state before:
pp: case right
X : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : HereditarilyLindelofSpace X
inst✝⁴ : LinearOrder E
inst✝³ : TopologicalSpace E
inst✝² : OrderClosedTopology E
inst✝¹ : DenselyOrdered E
inst✝ : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (X → E) → E → Set X := fun f d ↦ {x | f x < d}
U_open : ∀ {f : X → E}, f ∈ 𝓕 → ∀ (d : E), IsOpen (U f d)
this : ∀ (d : E), {x | s x < d} = ⋃ f, U (↑f) d
A : E → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), {x | s x < d} = ⋃ f ∈ A d, U f d
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
x : X
e : E
he : e ∈ lowerBounds (Function.eval x '' 𝓕')
H : s x < e
d : E
d_mem : d ∈ D
hd : d ∈ Ioo (s x) e
f : X → E
f_mem : f ∈ A d
hf : f x < d
⊢ e < e

Tactic:
exact (he (mem_image_of_mem _ (mem_iUnion₂_of_mem d_mem f_mem))).trans_lt hf |>.trans hd.2

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f : 𝕜 → 𝕜
⊢ logCounting f⁻¹ ⊤ = logCounting f 0

Tactic:
by
  simp [logCounting_zero, logCounting_top]

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inl.inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
xy : x ≤ y
zy : z ≤ y
⊢ HasConstantSpeedOnWith f (Icc x z) l

Tactic:
rintro u ⟨xu, uz⟩ v ⟨xv, vz⟩
      rw [Icc_inter_Icc, sup_of_le_right xu, inf_of_le_right vz, ←
        hfs ⟨xu, uz.trans zy⟩ ⟨xv, vz.trans zy⟩, Icc_inter_Icc, sup_of_le_right xu,
        inf_of_le_right (vz.trans zy)]

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

Goal state before:
pp: case refine_1
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 ≠ []
x✝ : ∃ l', l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
l' : List R
hl's : l'.SortedLE
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
⊢ List.Wbtw R l

Tactic:
rw [← hl'l]

Goal state after:
case refine_1
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 ≠ []
x✝ : ∃ l', l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
l' : List R
hl's : l'.SortedLE
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
⊢ List.Wbtw R (map (⇑(lineMap (l.head hl) (l.getLast hl))) l')
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case refine_1
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 ≠ []
x✝ : ∃ l', l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
l' : List R
hl's : l'.SortedLT
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
hla : l.length = 1 ∨ l.head hl ≠ l.getLast hl
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) l

Tactic:
rw [← hl'l]

Goal state after:
case refine_1
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 ≠ []
x✝ : ∃ l', l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
l' : List R
hl's : l'.SortedLT
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
hla : l.length = 1 ∨ l.head hl ≠ l.getLast hl
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (map (⇑(lineMap (l.head hl) (l.getLast hl))) l')
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 y z : P
h : y ∈ ⇑(lineMap x z) '' Set.Ioo 0 1 ∧ x ≠ z
⊢ Sbtw R x y z

Tactic:
rcases h with ⟨⟨t, ht, rfl⟩, hxz⟩

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
⊢ Sbtw R x ((lineMap x z) t) z
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case mp.inl
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
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : -(tx * (1 - ty)) = ty
h' : ty = 0
⊢ x = (lineMap x z) ty

Tactic:
simp [h']

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

Goal state before:
pp: case mp.inr
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
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : z -ᵥ x = 0
⊢ x = (lineMap x z) ty

Tactic:
vsub_eq_zero_iff_eq

Goal state after:
case mp.inr
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
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : z = x
⊢ x = (lineMap x z) ty
Module: Mathlib.CategoryTheory.CofilteredSystem

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

Tactic:
· rw [h, F.map_comp, types_comp]
    apply range_comp_subset_range

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x ↦ x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a b : α
hb : b ∈ s
ha : ¬a ∈ s
⊢ some b = some a ↔ False

Tactic:
simp [ne_of_mem_of_not_mem hb ha]

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
h : s = Set.univ
⊢ ofSet s = PEquiv.refl α

Tactic:
by simp only [← ofSet_univ, h]

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝⁵ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
this : (j : J) → Fintype (F.obj j)
⊢ ∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective ⇑(ConcreteCategory.hom (F.map f))

Tactic:
have : Fintype F.sections := Fintype.ofFinite F.sections

Goal state after:
J : Type u
inst✝⁵ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
this✝ : (j : J) → Fintype (F.obj j)
this : Fintype ↑F.sections
⊢ ∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective ⇑(ConcreteCategory.hom (F.map f))
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
v : n → R
inst✝ : CommRing R
⊢ Perm.permMatrix R σ *ᵥ v = v ∘ ⇑σ

Tactic:
ext j
  simp [mulVec_eq_sum, Pi.single, Function.update, Equiv.eq_symm_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

Goal state before:
pp: 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}
i j : n
⊢ ∀ i_1 ∈ univ, 0 ≤ (fun j ↦ M i j) i_1 * (fun j_1 ↦ N j_1 j) i_1

Tactic:
grind [mul_nonneg]

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✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x y z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
hx : (lineMap w y) t₁ = x
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
h_ne : 1 - t₁ + t₁ * t₂ = 0
h1 : t₁ = 1
⊢ x = y

Tactic:
← hx,

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
w x y z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
hx : (lineMap w y) t₁ = x
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
h_ne : 1 - t₁ + t₁ * t₂ = 0
h1 : t₁ = 1
⊢ (lineMap w y) t₁ = y
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
s✝ t : Set M
y : N
s : Set M
u v : N
hu : u ∈ {y | ∀ ⦃x : M⦄, x ∈ s → 0 ≤ (p x) y}
hv : v ∈ {y | ∀ ⦃x : M⦄, x ∈ s → 0 ≤ (p x) y}
x : M
hx : x ∈ s
⊢ 0 ≤ (p x) (u + v)

Tactic:
rw [map_add]

Goal state after:
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✝ t : Set M
y : N
s : Set M
u v : N
hu : u ∈ {y | ∀ ⦃x : M⦄, x ∈ s → 0 ≤ (p x) y}
hv : v ∈ {y | ∀ ⦃x : M⦄, x ∈ s → 0 ≤ (p x) y}
x : M
hx : x ∈ s
⊢ 0 ≤ (p x) u + (p x) v
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
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
⊢ ∃ e, ⇑e '' interior s = interior t ∧ ⇑e '' closure[inst✝³] s = closure[inst✝³] t

Tactic:
set h : E ≃ₜ E := by
    apply gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) <;>
      simp [← mem_interior_iff_mem_nhds, interior_vadd, mem_vadd_set_iff_neg_vadd_mem, *]

Goal state after:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ ∃ e, ⇑e '' interior s = interior t ∧ ⇑e '' closure[inst✝³] s = closure[inst✝³] t
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y ↦ 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
⊢ f y ≤ |r| + 2 * |f x₀| ∧ -f y ≤ |r| + 2 * |f x₀|

Tactic:
refine ⟨hfr.trans <| (le_abs_self _).trans <| by simp, ?_⟩

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y ↦ 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
⊢ -f y ≤ |r| + 2 * |f x₀|
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₁ t₂ : Set E
⊢ convexJoin 𝕜 (t₁ ∪ t₂) s = convexJoin 𝕜 t₁ s ∪ convexJoin 𝕜 t₂ s

Tactic:
convexJoin_union_left

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : LocallyLipschitzOn C f → ContinuousOn f C
tfae_2_to_3 : ContinuousOn f C → ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : (∃ x₀ ∈ C, ContinuousAt f x₀) → ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) f
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
x : E
hx : x ∈ C
this : ∀ᶠ (δ : ℝ) in 𝓝 0, (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C
δ : ℝ
hδ₀ : 0 < δ
hδ₁ : δ < 1
y : E := (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀
hy : y ∈ C
hr✝ : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
ε : ℝ
hε : ε > 0
hr : ∀ ⦃y : E⦄, dist y x₀ < ε → f y ≤ r ∧ y ∈ C
z : E
hz : dist z x < ε * δ
hx₀' : δ⁻¹ • (x - y) + y = x₀
w : E := δ⁻¹ • (z - y) + y
⊢ δ • w + (1 - δ) • y = z

Tactic:
simp [w, hδ₀.ne', sub_smul]

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

Goal state before:
pp: case refine_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : E
hxs : x ∈ s
hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂
y : E
hyt : y ∈ t
hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂
⊢ 0 ≤ p * a₁ + q * a₂

Tactic:
try positivity

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

Goal state before:
pp: case refine_2
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : E
hxs : x ∈ s
hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂
y : E
hyt : y ∈ t
hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂
⊢ 0 ≤ p * b₁ + q * b₂

Tactic:
try positivity

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

Goal state before:
pp: case refine_3
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : E
hxs : x ∈ s
hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂
y : E
hyt : y ∈ t
hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂
⊢ p * a₁ + q * a₂ + (p * b₁ + q * b₂) = 1

Tactic:
try positivity

Goal state after:
case refine_3
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : E
hxs : x ∈ s
hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂
y : E
hyt : y ∈ t
hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂
⊢ p * a₁ + q * a₂ + (p * b₁ + q * b₂) = 1
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: case refine_4
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : E
hxs : x ∈ s
hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂
y : E
hyt : y ∈ t
hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂
⊢ (p * a₁ + q * a₂) • x + (p * b₁ + q * b₂) • y = p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂)

Tactic:
try positivity

Goal state after:
case refine_4
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : E
hxs : x ∈ s
hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂
y : E
hyt : y ∈ t
hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂
⊢ (p * a₁ + q * a₂) • x + (p * b₁ + q * b₂) • y = p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂)
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
⊢ (fun a ↦ ↑a) '' (closure[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s) \ frontier (Subtype.val ⁻¹' s)) =
    intrinsicInterior 𝕜 s

Tactic:
closure_sdiff_frontier,

Goal state after:
𝕜 : 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
⊢ (fun a ↦ ↑a) '' interior (Subtype.val ⁻¹' s) = intrinsicInterior 𝕜 s