mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: 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
⊢ ∃ i_1 f,
    ∀ ⦃k : J⦄ (g : k ⟶ i_1),
      range ⇑(ConcreteCategory.hom ((F.toPreimages s).map f)) ⊆
        range ⇑(ConcreteCategory.hom ((F.toPreimages s).map (g ≫ f)))

Tactic:
obtain ⟨j₁, g₁, f₁, -⟩ := IsCofilteredOrEmpty.cone_objs i j

Goal state after:
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
⊢ ∃ i_1 f,
    ∀ ⦃k : J⦄ (g : k ⟶ i_1),
      range ⇑(ConcreteCategory.hom ((F.toPreimages s).map f)) ⊆
        range ⇑(ConcreteCategory.hom ((F.toPreimages s).map (g ≫ f)))
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring α
f : l ≃. m
i : l
j : n
M : Matrix m n α
⊢ ∑ j_1, (if j_1 ∈ f i then 1 else 0) * M j_1 j = Option.rec 0 (fun val ↦ M val j) (f i)

Tactic:
rcases h : f i with - | fi

Goal state after:
case none
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring α
f : l ≃. m
i : l
j : n
M : Matrix m n α
h : f i = none
⊢ ∑ j_1, (if j_1 ∈ none then 1 else 0) * M j_1 j = Option.rec 0 (fun val ↦ M val j) none

case some
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring α
f : l ≃. m
i : l
j : n
M : Matrix m n α
fi : m
h : f i = some fi
⊢ ∑ j_1, (if j_1 ∈ some fi then 1 else 0) * M j_1 j = Option.rec 0 (fun val ↦ M val j) (some fi)
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) ∧ M *ᵥ 1 = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1}
⊢ (M * N) *ᵥ 1 = 1

Tactic:
← mulVec_mulVec,

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✝
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) ∧ M *ᵥ 1 = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1}
⊢ M *ᵥ N *ᵥ 1 = 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✝⁵ : 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₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : p ∈ line[R, t.points i₁, p₁]
h₂' : p ∈ line[R, t.points i₂, p₂]
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
⊢ Sbtw R (t.points i₁) p p₁

Tactic:
have hp : p ∈ affineSpan R (Set.range t.points) := by
    have hle : line[R, t.points i₁, p₁] ≤ affineSpan R (Set.range t.points) := by
      refine affineSpan_pair_le_of_mem_of_mem (mem_affineSpan R (Set.mem_range_self _)) ?_
      have hle : line[R, t.points i₂, t.points i₃] ≤ affineSpan R (Set.range t.points) := by
        refine affineSpan_mono R ?_
        simp [Set.insert_subset_iff]
      rw [AffineSubspace.le_def'] at hle
      exact hle _ h₁.wbtw.mem_affineSpan
    rw [AffineSubspace.le_def'] at hle
    exact hle _ h₁'

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₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : p ∈ line[R, t.points i₁, p₁]
h₂' : p ∈ line[R, t.points i₂, p₂]
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
hp : p ∈ affineSpan R (Set.range t.points)
⊢ Sbtw R (t.points i₁) p p₁
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✝
M✝ : Matrix n✝ 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) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
⊢ (M * N) *ᵥ 1 = 1

Tactic:
← mulVec_mulVec,

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✝
M✝ : Matrix n✝ 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) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
⊢ M *ᵥ N *ᵥ 1 = 1
Module: Mathlib.Analysis.Convex.Body

Goal state before:
pp: 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
⊢ a • K ≤ b • K

Tactic:
rw [← SetLike.coe_subset_coe, coe_smul', coe_smul']

Goal state after:
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
⊢ a • ↑K ⊆ b • ↑K
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
h : ¬AffineIndependent 𝕜 Subtype.val
x : E
m : x ∈ (convexHull 𝕜) ↑t
⊢ ∃ y, x ∈ (convexHull 𝕜) ↑(t.erase ↑y)

Tactic:
simp only [Finset.convexHull_eq, mem_ofPred_eq] at m ⊢
  obtain ⟨f, fpos, fsum, rfl⟩ := m
  obtain ⟨g, gcombo, gsum, gpos⟩ := exists_nontrivial_relation_sum_zero_of_not_affine_ind h
  replace gpos := exists_pos_of_sum_zero_of_exists_nonzero g gsum gpos
  clear h
  let s := {z ∈ t | 0 < g z}
  obtain ⟨i₀, mem, w⟩ : ∃ i₀ ∈ s, ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i := by
    apply s.exists_min_image fun z => f z / g z
    obtain ⟨x, hx, hgx⟩ : ∃ x ∈ t, 0 < g x := gpos
    exact ⟨x, mem_filter.mpr ⟨hx, hgx⟩⟩
  have hg : 0 < g i₀ := by
    rw [mem_filter] at mem
    exact mem.2
  have hi₀ : i₀ ∈ t := filter_subset _ _ mem
  let k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
  have hk : k i₀ = 0 := by simp [k, ne_of_gt hg]
  have ksum : ∑ e ∈ t.erase i₀, k e = 1 := by
    calc
      ∑ e ∈ t.erase i₀, k e = ∑ e ∈ t, k e := by
        conv_rhs => rw [← insert_erase hi₀, sum_insert (notMem_erase i₀ t), hk, zero_add]
      _ = ∑ e ∈ t, (f e - f i₀ / g i₀ * g e) := rfl
      _ = 1 := by rw [sum_sub_distrib, fsum, ← mul_sum, gsum, mul_zero, sub_zero]
  refine ⟨⟨i₀, hi₀⟩, k, ?_, by convert! ksum, ?_⟩
  · simp only [k, and_imp, sub_nonneg, mem_erase, Ne]
    intro e _ het
    by_cases hes : e ∈ s
    · have hge : 0 < g e := by
        rw [mem_filter] at hes
        exact hes.2
      rw [← le_div_iff₀ hge]
      exact w _ hes
    · calc
        _ ≤ 0 := by
          apply mul_nonpos_of_nonneg_of_nonpos
          · apply div_nonneg (fpos i₀ (mem_of_subset (filter_subset _ t) mem)) (le_of_lt hg)
          · simpa only [s, mem_filter, het, true_and, not_lt] using hes
        _ ≤ f e := fpos e het
  · rw [Subtype.coe_mk, centerMass_eq_of_sum_1 _ id ksum]
    calc
      ∑ e ∈ t.erase i₀, k e • e = ∑ e ∈ t, k e • e := sum_erase _ (by rw [hk, zero_smul])
      _ = ∑ e ∈ t, (f e - f i₀ / g i₀ * g e) • e := rfl
      _ = t.centerMass f id := by
        simp only [sub_smul, mul_smul, sum_sub_distrib, ← smul_sum, gcombo, smul_zero, sub_zero,
          centerMass, fsum, inv_one, one_smul, id]

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

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

Tactic:
exact ht₂.comp_embedding ⟨_, inclusion_injective (Finset.filter_subset (fun i => w i ≠ 0) t)⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : LinearOrder R
inst✝⁸ : IsStrictOrderedRing R
G : Type u_2
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
H : Type u_3
inst✝⁵ : AddCommGroup H
inst✝⁴ : Module R H
G' : Type u_4
H' : Type u_5
inst✝³ : AddCommGroup G'
inst✝² : Module R G'
inst✝¹ : AddCommGroup H'
inst✝ : Module R H'
f : G →ₗ[R] G'
g : H →ₗ[R] H'
C₁ : PointedCone R G
C₂ : PointedCone R H
⊢ map (TensorProduct.map f g) (C₁.maxTensorProduct C₂) ≤ (map f C₁).maxTensorProduct (map g C₂)

Tactic:
rintro _ ⟨w, hw, rfl⟩

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : LinearOrder R
inst✝⁸ : IsStrictOrderedRing R
G : Type u_2
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
H : Type u_3
inst✝⁵ : AddCommGroup H
inst✝⁴ : Module R H
G' : Type u_4
H' : Type u_5
inst✝³ : AddCommGroup G'
inst✝² : Module R G'
inst✝¹ : AddCommGroup H'
inst✝ : Module R H'
f : G →ₗ[R] G'
g : H →ₗ[R] H'
C₁ : PointedCone R G
C₂ : PointedCone R H
w : G ⊗[R] H
hw : w ∈ ↑(C₁.maxTensorProduct C₂)
⊢ (↑{ c // 0 ≤ c } (TensorProduct.map f g)) w ∈ (map f C₁).maxTensorProduct (map g C₂)
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
hB : B.Nonempty
⊢ ∃ l a, B = {x | x ∈ A ∧ a ≤ l x}

Tactic:
obtain ⟨l, rfl⟩ := hAB hB

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
l : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hB : {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}.Nonempty
⊢ ∃ l_1 a, {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} = {x | x ∈ A ∧ a ≤ l_1 x}
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
x : E
⊢ gaugeRescale s s x = x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inl
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
⊢ gaugeRescale s s 0 = 0

case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
x : E
hx : x ≠ 0
⊢ gaugeRescale s s x = x
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
⊢ gauge t (gaugeRescale s t x) = gauge s x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inl
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
⊢ gauge t (gaugeRescale s t 0) = gauge s 0

case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ gauge t (gaugeRescale s t x) = gauge s x
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
⊢ gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inl
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
⊢ gaugeRescale t u (gaugeRescale s t 0) = gaugeRescale s u 0

case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 A C
hCB : C ⊆ B
⊢ IsExposed 𝕜 (A ∩ B) C

Tactic:
rintro ⟨w, hw⟩
  obtain ⟨l, rfl⟩ := hC ⟨w, hw⟩
  exact ⟨l, Subset.antisymm (fun x hx => ⟨⟨hx.1, hCB hx⟩, fun y hy => hx.2 y hy.1⟩)
    fun x ⟨⟨hxC, _⟩, hx⟩ => ⟨hxC, fun y hy => (hw.2 y hy).trans (hx w ⟨hC.subset hw, hCB hw⟩)⟩⟩

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

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : Ring 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
hA : Convex 𝕜 A
hB : B.Nonempty
⊢ Convex 𝕜 B

Tactic:
obtain ⟨l, rfl⟩ := hAB hB

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : Ring 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
hA : Convex 𝕜 A
l : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hB : {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}.Nonempty
⊢ Convex 𝕜 {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
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
hs : Convex ℝ s
hs₀ : s ∈ 𝓝 0
ht : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ Continuous[inst✝³, inst✝³] (gaugeRescale s t)

Tactic:
have hta : Absorbent ℝ t := absorbent_nhds_zero ht₀

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
hs : Convex ℝ s
hs₀ : s ∈ 𝓝 0
ht : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
hta : Absorbent ℝ t
⊢ Continuous[inst✝³, inst✝³] (gaugeRescale s t)
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
hs : Convex ℝ s
hs₀ : s ∈ 𝓝 0
ht : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
hta : Absorbent ℝ t
x : E
⊢ ContinuousAt (gaugeRescale s t) x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

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
⊢ ContinuousAt (gaugeRescale s t) 0

case inr
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
x : E
hx : x ≠ 0
⊢ ContinuousAt (gaugeRescale s t) x
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst✝ : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : α → E
hgm : StronglyMeasurable g
hfg : f =ᵐ[μ] g
this : SeparableSpace ↑(range g ∩ s)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
⊢ ∫ (a : α), g a ∂μ ∈ s

Tactic:
integrable_congr hfg

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst✝ : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᵐ[μ] g
this : SeparableSpace ↑(range g ∩ s)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
⊢ ∫ (a : α), g a ∂μ ∈ s
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: 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

Tactic:
have h := hf_cvx.continuousOn_interior x
    simp only [nonempty_Iio, interior_Ici', mem_Ioi] at h
    rw [continuousWithinAt_iff_continuousAt (Ioi_mem_nhds hxy)] at h
    exact (h hxy).continuousWithinAt

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

Goal state before:
pp: V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
p' : ↥(_root_.affineSpan ℝ s) := ⟨p, ⋯⟩
⊢ Convex ℝ (⇑(AffineIsometryEquiv.constVSub ℝ p').symm.toHomeomorph ⁻¹' Subtype.val ⁻¹' s)

Tactic:
exact hscv.affine_preimage
    ((_root_.affineSpan ℝ s).subtype.comp
      (AffineIsometryEquiv.constVSub ℝ p').symm.toAffineEquiv.toAffineMap)

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
⊢ convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair t'' s'' ht'' hs'' ⋯ m₂ m₁) m₃ =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃

Tactic:
convexCombPair_symm (x := m₂)

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
⊢ convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' ⋯ m₁ m₂) m₃ =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
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 : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
x✝¹ : x ∈ Set.univ
y : E
x✝ : y ∈ Set.univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : e < a • x + b • y
hc' : a • x + b • y ≤ a • e + b • y
⊢ g (a • x + b • y) ≤ a • g e + b • g y

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 : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
x✝¹ : x ∈ Set.univ
y : E
x✝ : y ∈ Set.univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : e < a • x + b • y
hc' : a • x + b • y ≤ a • e + b • y
⊢ a • g e + b • g y ≤ a • f x + b • g y

Tactic:
· exact (h_mono hc.le (hc.le.trans hc') hc').trans (hg.2 Set.self_mem_Ici hy.le ha hb hab)

Goal state after:
𝕜 : 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 : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
x✝¹ : x ∈ Set.univ
y : E
x✝ : y ∈ Set.univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : e < a • x + b • y
hc' : a • x + b • y ≤ a • e + b • y
⊢ a • g e + b • g y ≤ a • f x + b • g y
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
⊢ 0 ≤ 1 - ↑i

Tactic:
simpa using i.prop.right

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

Goal state before:
pp: case neg.inl
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 0
⊢ ∀ (i : ℝ),
    0 < i → ∀ᶠ (x_1 : T) in nhds t, convexCombPair (f x_1) (1 - f x_1) ⋯ ⋯ ⋯ (x x_1) (y x_1) ∈ Metric.ball (y t) i

Tactic:
intro r hr

Goal state after:
case neg.inl
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 0
r : ℝ
hr : 0 < r
⊢ ∀ᶠ (x_1 : T) in nhds t, convexCombPair (f x_1) (1 - f x_1) ⋯ ⋯ ⋯ (x x_1) (y x_1) ∈ Metric.ball (y t) r