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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
s t : Set (OnePoint X)
⊢ (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen[inst✝] (some ⁻¹' s) →
    (∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ) ∧ IsOpen[inst✝] (some ⁻¹' t) →
      (∞ ∈ s ∩ t → IsCompact (some ⁻¹' (s ∩ t))ᶜ) ∧ IsOpen[inst✝] (some ⁻¹' (s ∩ t))

Tactic:
rintro ⟨hms, hs⟩ ⟨hmt, ht⟩
    refine ⟨?_, hs.inter ht⟩
    rintro ⟨hms', hmt'⟩
    simpa [compl_inter] using (hms hms').union (hmt hmt')

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
this : ∞ ∉ sᶜ
⊢ IsOpen[inst✝] (some ⁻¹' sᶜ) ↔ IsOpen[inst✝] (some ⁻¹' s)ᶜ

Tactic:
preimage_compl

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
this : ∞ ∉ sᶜ
⊢ IsOpen[inst✝] (some ⁻¹' s)ᶜ ↔ IsOpen[inst✝] (some ⁻¹' s)ᶜ
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : UCompactlyGeneratedSpace X
f : X → Y
hf : Continuous[tX, tY] f
ht : tY = coinduced f tX
s : Set Y
h : ∀ (S : CompHaus) (f : C(↑S.toTop, Y)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed[tX] (f ⁻¹' s)

Tactic:
exact UCompactlyGeneratedSpace.isClosed fun _ ⟨g, hg⟩ ↦ h _ ⟨_, hf.comp hg⟩

Goal state after:
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)
this : Tendsto some (cocompact X) (𝓝 ∞)
⊢ IsCompact univ

Tactic:
rw [← insert_none_range_some X]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
this : Tendsto some (cocompact X) (𝓝 ∞)
⊢ IsCompact (insert none (range Option.some))
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)
⊢ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ ≤ ‖2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)‖

Tactic:
norm_of_nonneg h_bound_nonneg

Goal state after:
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)
⊢ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inl.inl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal (↑l * (y - z))

Tactic:
have : (s ∪ t) ∩ Icc z y = s ∩ Icc z y := by
      ext w; constructor
      · rintro ⟨ws | wt, zw, wy⟩
        · exact ⟨ws, zw, wy⟩
        · exact ⟨(le_antisymm (wy.trans (hs.2 ys)) (ht.2 wt)).symm ▸ hs.1, zw, wy⟩
      · rintro ⟨ws, zwy⟩; exact ⟨Or.inl ws, zwy⟩

Goal state after:
case inl.inl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z y
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal (↑l * (y - z))
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ logCounting (f₁ * f₂) 0 r ≤ (logCounting f₁ 0 + logCounting f₂ 0) r

Tactic:
by
  simp only [logCounting, WithTop.zero_ne_top, reduceDIte, WithTop.untop₀_zero, sub_zero]
  rw [divisor_mul h₁f₁.meromorphicOn h₁f₂.meromorphicOn (fun z _ ↦ h₂f₁ z) (fun z _ ↦ h₂f₂ z),
    ← locallyFinsuppWithin.logCounting.map_add]
  apply locallyFinsuppWithin.logCounting_le _ hr
  apply locallyFinsuppWithin.posPart_add

Goal state after:
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'
hf : Function.Injective ⇑f
⊢ List.Wbtw R l ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (map (⇑f) l) ↔ List.Wbtw R l ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) l

Tactic:
refine ⟨fun ⟨hl, hp⟩ ↦ ⟨hl, hp.of_map _ ?_⟩, fun ⟨hl, hp⟩ ↦ ⟨hl, hp.map _ ?_⟩⟩

Goal state after:
case refine_1
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'
hf : Function.Injective ⇑f
x✝ : List.Wbtw R l ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (map (⇑f) l)
hl : List.Wbtw R l
hp : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (map (⇑f) l)
⊢ ∀ (a b : P), f a ≠ f b → a ≠ b

case refine_2
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'
hf : Function.Injective ⇑f
x✝ : List.Wbtw R l ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
hl : List.Wbtw R l
hp : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
⊢ ∀ (a b : P), a ≠ b → f a ≠ f b
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case neg.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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2)) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2)) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw R ((lineMap head (tail.getLast ht2)) r :: tail)
ht : ¬(lineMap head (tail.getLast ht2)) r :: tail = []
hl'' :
  map (⇑(lineMap ((lineMap head (tail.getLast ht2)) r) (tail.getLast ht2))) l'' =
    (lineMap head (tail.getLast ht2)) r :: tail
⊢ (0 :: map (fun x ↦ r + (1 - r) * x) l'').SortedLE

pp: case neg.refine_3
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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2)) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2)) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw R ((lineMap head (tail.getLast ht2)) r :: tail)
ht : ¬(lineMap head (tail.getLast ht2)) r :: tail = []
hl'' :
  map (⇑(lineMap ((lineMap head (tail.getLast ht2)) r) (tail.getLast ht2))) l'' =
    (lineMap head (tail.getLast ht2)) r :: tail
⊢ map (⇑(lineMap head (tail.getLast ht2))) (0 :: map (fun x ↦ r + (1 - r) * x) l'') =
    head :: (lineMap head (tail.getLast ht2)) r :: tail

Tactic:
· simp only [sortedLE_iff_pairwise, pairwise_cons, mem_map,
                forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
              refine ⟨?_, ?_⟩
              · intro a ha
                have := hl''0 a ha
                nlinarith
              · refine hl''s.pairwise.map _ fun a b hab ↦ ?_
                gcongr

Goal state after:
case neg.refine_3
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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2)) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2)) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw R ((lineMap head (tail.getLast ht2)) r :: tail)
ht : ¬(lineMap head (tail.getLast ht2)) r :: tail = []
hl'' :
  map (⇑(lineMap ((lineMap head (tail.getLast ht2)) r) (tail.getLast ht2))) l'' =
    (lineMap head (tail.getLast ht2)) r :: tail
⊢ map (⇑(lineMap head (tail.getLast ht2))) (0 :: map (fun x ↦ r + (1 - r) * x) l'') =
    head :: (lineMap head (tail.getLast ht2)) r :: tail
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_1
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
x y : P
h : Wbtw R x y x
⊢ y = x

Tactic:
simpa [Wbtw, affineSegment] using h

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
w x y z : P
h₁ : Wbtw R w y z
h₂ : Sbtw R w x y
⊢ Sbtw R w x z

Tactic:
refine ⟨h₁.trans_left h₂.wbtw, h₂.ne_left, ?_⟩
  rintro rfl
  exact h₂.right_ne ((wbtw_swap_right_iff R w).1 ⟨h₁, h₂.wbtw⟩)

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
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
⊢ (ConcreteCategory.hom (F.map f₂)) x ∈ F.eventualRange j₁

Tactic:
rw [h₂]

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
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
⊢ (ConcreteCategory.hom (F.map f₂)) x ∈ range ⇑(ConcreteCategory.hom (F.map f₂))
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
σ : Equiv.Perm n
⊢ (∀ (i j : n), 0 ≤ Equiv.Perm.permMatrix R σ i j) ∧ ∀ (i : n), ∑ j, Equiv.Perm.permMatrix R σ i j = 1

Tactic:
refine ⟨fun i j => ?g1, ?g2⟩

Goal state after:
case g1
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
σ : Equiv.Perm n
i j : n
⊢ 0 ≤ Equiv.Perm.permMatrix R σ i j

case g2
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
σ : Equiv.Perm n
⊢ ∀ (i : n), ∑ j, Equiv.Perm.permMatrix R σ i j = 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
σ : Equiv.Perm n
⊢ (∀ (i j : n), 0 ≤ Equiv.Perm.permMatrix R σ i j) ∧ ∀ (j : n), ∑ i, Equiv.Perm.permMatrix R σ i j = 1

Tactic:
refine ⟨fun i j => ?g1, ?g2⟩

Goal state after:
case g1
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
σ : Equiv.Perm n
i j : n
⊢ 0 ≤ Equiv.Perm.permMatrix R σ i j

case g2
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
σ : Equiv.Perm n
⊢ ∀ (j : n), ∑ i, Equiv.Perm.permMatrix R σ i j = 1
Module: Mathlib.Analysis.Convex.Birkhoff

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 < s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
f : n → Finset n := ⋯
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s
h₂ : ∑ i, ∑ j ∈ A.biUnion f, M i j = ↑(#(A.biUnion f)) * s
⊢ ∑ i ∈ A, ∑ j ∈ f i, M i j ≤ ∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j

Tactic:
refine sum_le_sum fun i hi => ?_

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 < s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
f : n → Finset n := fun i ↦ {j | M i j ≠ 0}
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s
h₂ : ∑ i, ∑ j ∈ A.biUnion f, M i j = ↑(#(A.biUnion f)) * s
i : n
hi : i ∈ A
⊢ ∑ j ∈ f i, M i j ≤ ∑ j ∈ A.biUnion f, M i j
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:
← SetLike.coe_subset_coe,

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.Between

Goal state before:
pp: case refine_1.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 z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ x = (lineMap x z) r ∨ z ∈ ⇑(lineMap x ((lineMap x z) r)) '' Set.Ici 1

pp: case refine_1.inr
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 z : P
hr0 : 0 ≤ 0
hr1 : 0 ≤ 1
⊢ x = (lineMap x z) 0 ∨ z ∈ ⇑(lineMap x ((lineMap x z) 0)) '' Set.Ici 1

Tactic:
· rw [Set.mem_image]
      refine .inr ⟨r⁻¹, (one_le_inv₀ hr0').2 hr1, ?_⟩
      simp only [lineMap_apply, smul_smul, vadd_vsub]
      rw [inv_mul_cancel₀ hr0'.ne', one_smul, vsub_vadd]

Goal state after:
case refine_1.inr
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 z : P
hr0 : 0 ≤ 0
hr1 : 0 ≤ 1
⊢ x = (lineMap x z) 0 ∨ z ∈ ⇑(lineMap x ((lineMap x z) 0)) '' Set.Ici 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
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ ∃ ι x_1 z w, Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i, w i = 1 ∧ ∑ i, w i • z i = x

Tactic:
rw [convexHull_eq_union] at hx
  simp only [exists_prop, Set.mem_iUnion] at hx
  obtain ⟨t, ht₁, ht₂, ht₃⟩ := hx
  simp only [t.convexHull_eq, Set.mem_ofPred_eq] at ht₃
  obtain ⟨w, hw₁, hw₂, hw₃⟩ := ht₃
  let t' := {i ∈ t | w i ≠ 0}
  refine ⟨t', t'.fintypeCoeSort, ((↑) : t' → E), w ∘ ((↑) : t' → E), ?_, ?_, ?_, ?_, ?_⟩
  · rw [Subtype.range_coe_subtype]
    exact Subset.trans (Finset.filter_subset _ t) ht₁
  · exact ht₂.comp_embedding ⟨_, inclusion_injective (Finset.filter_subset (fun i => w i ≠ 0) t)⟩
  · exact fun i =>
      (hw₁ _ (Finset.mem_filter.mp i.2).1).lt_of_ne (Finset.mem_filter.mp i.property).2.symm
  · simp only [univ_eq_attach, Function.comp_apply]
    rw [Finset.sum_attach, Finset.sum_filter_ne_zero, hw₂]
  · change (∑ i ∈ t'.attach, (fun e => w e • e) ↑i) = x
    rw [Finset.sum_attach (f := fun e => w e • e), Finset.sum_filter_of_ne]
    · rw [t.centerMass_eq_of_sum_1 id hw₂] at hw₃
      exact hw₃
    · intro e _ hwe contra
      apply hwe
      rw [contra, zero_smul]

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

Goal state before:
pp: case inl
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
h✝ : IsEmpty n
⊢ ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ = 1 ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M

pp: case inr
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
h✝ : Nonempty n
⊢ ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ = 1 ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
case inl => exact ⟨fun _ => 1, by simp, by simp, Subsingleton.elim _ _⟩

Goal state after:
case inr
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
h✝ : Nonempty n
⊢ ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ = 1 ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
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✝¹¹ : IsOrderedRing R
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : ClosedIciTopology R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝² : p.IsContPerfPair
inst✝¹ : IsTopologicalRing R
inst✝ : T1Space N
⊢ dual p univ = ⊥

Tactic:
refine le_antisymm (fun y hy ↦ (_root_.map_eq_zero_iff _ p.flip.toContPerfPair.injective).1 ?_)
    (by simp)

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsOrderedRing R
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : ClosedIciTopology R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝² : p.IsContPerfPair
inst✝¹ : IsTopologicalRing R
inst✝ : T1Space N
y : N
hy : y ∈ dual p univ
⊢ p.flip.toContPerfPair y = 0
Module: Mathlib.Analysis.Convex.Measure

Goal state before:
pp: case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
hspan : affineSpan ℝ s ≠ ⊤
⊢ frontier s ⊆ ↑(affineSpan ℝ s)

Tactic:
exact frontier_subset_closure.trans
      (closure_minimal (subset_affineSpan _ _) (affineSpan ℝ s).closed_of_finiteDimensional)

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

Goal state before:
pp: f : ℝ → ℝ
y z : ℝ
hf_cnv : ConcaveOn ℝ (Ico y z) f
hf_cont : ContinuousWithinAt f (Ici y) y
⊢ ContinuousOn f (Ico y z)

Tactic:
simpa using hf_cnv.neg.continuousOn_Ico hf_cont.neg

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
x : P
⊢ convexCombination (StdSimplex.single x) = x

Tactic:
by
  simp only [convexCombination, StdSimplex.single]
  rw [Finsupp.support_single _ one_ne_zero]
  exact ({x} : Finset P).affineCombination_of_eq_one_of_eq_zero _ _
    (Finset.mem_singleton_self x) Finsupp.single_eq_same fun j _ hne => Finsupp.single_eq_of_ne hne

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

Goal state before:
pp: I : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst✝¹ : Zero X
inst✝ : ConvexSpace R X
i✝ : ι
w : StdSimplex R (ι →₀ X)
i : ι
hi : (iConvexComb w fun x ↦ x i) ≠ 0
⊢ i ∈ w.weights.support.biUnion support

Tactic:
contrapose! hi

Goal state after:
I : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst✝¹ : Zero X
inst✝ : ConvexSpace R X
i✝ : ι
w : StdSimplex R (ι →₀ X)
i : ι
hi : i ∉ w.weights.support.biUnion support
⊢ (iConvexComb w fun x ↦ x i) = 0
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 α
f : α → E
C : ℝ
inst✝¹ : StrictConvexSpace ℝ E
inst✝ : IsFiniteMeasure μ
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖∫ (x : α), f x ∂μ‖ < μ.real univ * C

Tactic:
by
  rcases eq_or_ne μ 0 with h₀ | h₀; · simp [h₀, EventuallyEq]
  have hμ : 0 < μ.real univ := by
    simp [measureReal_def, ENNReal.toReal_pos_iff, pos_iff_ne_zero, h₀, measure_lt_top]
  refine (ae_eq_const_or_norm_average_lt_of_norm_le_const h_le).imp_right fun H => ?_
  rwa [average_eq, norm_smul, norm_inv, Real.norm_eq_abs, abs_of_pos hμ, ← div_eq_inv_mul,
    div_lt_iff₀' hμ] at H

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
⊢ IsConvexSet R ∅

Tactic:
by simp [IsConvexSet]

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
⊢ IsConvexSet R univ

Tactic:
by simp [IsConvexSet]

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

Goal state before:
pp: X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
f : StdSimplex ℝ X
x : X
⊢ dist (sConvexComb f) x ≤ iConvexComb f fun x_1 ↦ dist x_1 x

Tactic:
by
  simpa using dist_iConvexComb_left_le f id x

Goal state after: