mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case cons.refine_2.refine_2
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
head : P
tail : List P
x✝ : (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) tail
ha : ∀ (a : P), head :: tail ≠ [a, a]
ht' : List.Wbtw R tail
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ ∀ (a : P), tail ≠ [a, a]
a : P
⊢ tail ≠ [a, a]

Tactic:
· rintro rfl
        simp at hp

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

Goal state before:
pp: case refine_1
𝕜 : 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
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
x : ↑s
⊢ (range fun f ↦ ↑f x).Nonempty

Tactic:
obtain ⟨l, c, hlc⟩ := exists_affine_le_of_lt (𝕜 := 𝕜) x.2 (show φ x - 1 < φ x by grind)
      hsc hφc hφcv

Goal state after:
case refine_1
𝕜 : 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
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
x : ↑s
l : E →L[𝕜] 𝕜
c : ℝ
hlc : s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c ≤ s.domRestrict φ ∧ re (l ↑x) + c = φ ↑x - 1
⊢ (range fun f ↦ ↑f x).Nonempty
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
x✝ : ∃ p₁ p₂ l', l'.SortedLE ∧ map (⇑(lineMap p₁ p₂)) l' = l
p₁ p₂ : P
l' : List R
hl's : l'.SortedLE
hl'l : map (⇑(lineMap p₁ p₂)) l' = l
⊢ List.Wbtw R l

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
h : List.Wbtw R l
⊢ ∃ p₁ p₂ l', l'.SortedLE ∧ map (⇑(lineMap p₁ p₂)) l' = l

Tactic:
· subst hl'l
    exact Wbtw.map hl's.wbtw _

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
h : List.Wbtw R l
⊢ ∃ p₁ p₂ l', l'.SortedLE ∧ map (⇑(lineMap p₁ p₂)) l' = l
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case refine_1
𝕜 : 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.Nonempty
𝓕 : Set (↑s → ℝ) := {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c}
⊢ 𝓕.Nonempty

pp: case refine_2
𝕜 : 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.Nonempty
𝓕 : Set (↑s → ℝ) := {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c}
⊢ BddAbove 𝓕

Tactic:
· obtain ⟨l, c, hlc⟩ := exists_affine_le_of_lt (𝕜 := 𝕜) hs.some_mem
          (by grind : φ hs.some - 1 < φ (⟨hs.some, hs.some_mem⟩ : s)) hsc hφc hφcv
        exact ⟨s.domRestrict (re ∘ l) + const s c, hlc.1, l, c, rfl⟩

Goal state after:
case refine_2
𝕜 : 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.Nonempty
𝓕 : Set (↑s → ℝ) := {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c}
⊢ BddAbove 𝓕
Module: Mathlib.Analysis.Convex.Approximation

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

Tactic:
by_cases! hs : s.Nonempty
  · let 𝓕 := {f | f ≤ s.domRestrict φ ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ), f = s.domRestrict (re ∘ l) + const s c}
    have hl : IsLUB 𝓕 (s.domRestrict φ) := by
      refine (hφcv.sSup_affine_eq (𝕜 := 𝕜) hsc hφc) ▸ isLUB_csSup ?_ ?_
      · obtain ⟨l, c, hlc⟩ := exists_affine_le_of_lt (𝕜 := 𝕜) hs.some_mem
          (by grind : φ hs.some - 1 < φ (⟨hs.some, hs.some_mem⟩ : s)) hsc hφc hφcv
        exact ⟨s.domRestrict (re ∘ l) + const s c, hlc.1, l, c, rfl⟩
      · exact (bddAbove_def.2 ⟨φ ∘ Subtype.val, fun y hy => hy.1⟩)
    have hr (f) (hf : f ∈ 𝓕) : LowerSemicontinuous f := by
      obtain ⟨l, c, hlc⟩ := hf.2
      exact Continuous.lowerSemicontinuous (hlc ▸ by fun_prop)
    obtain ⟨𝓕', h𝓕'⟩ := exists_countable_lowerSemicontinuous_isLUB hr hl
    refine ⟨𝓕', h𝓕'.2.1, h𝓕'.2.2.csSup_eq ?_, fun f hf => h𝓕'.1 hf⟩
    by_contra!
    grind [(isLUB_empty_iff.1 (this ▸ h𝓕'.2.2)) (fun x : s => φ x - 1) ⟨hs.some, hs.some_mem⟩]
  · use ∅; simp [domRestrict_def]; grind

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

Goal state before:
pp: case intro.ind.zero
α : Type v
inst✝¹ : DecidableEq α
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val✝ : Fintype ι
ih :
  ∀ m < 0,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι],
      (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) →
        ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = 0
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
rw [Fintype.card_eq_zero_iff] at hn

Goal state after:
case intro.ind.zero
α : Type v
inst✝¹ : DecidableEq α
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val✝ : Fintype ι
ih :
  ∀ m < 0,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι],
      (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) →
        ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : IsEmpty ι
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Module: Mathlib.Analysis.Convex.Approximation

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

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

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✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
w : Fin (1 + 1) → R
hw : w 0 + w 1 = 1
h01 : ∀ (i : Fin (1 + 1)), w i ∈ Set.Icc 0 1
i : Fin (1 + 1)
⊢ w i = Finset.affineCombinationLineMapWeights 0 1 (w 1) i

Tactic:
fin_cases i <;> simp [← hw]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) := {f | f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c}
⊢ IsLUB 𝓕 φ

Tactic:
refine (hφcv.univ_sSup_affine_eq (𝕜 := 𝕜) hφc) ▸ isLUB_csSup ?_ ?_

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) := {f | f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c}
⊢ 𝓕.Nonempty

case refine_2
𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) := {f | f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c}
⊢ BddAbove 𝓕
Module: Mathlib.CategoryTheory.CofilteredSystem

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

Tactic:
obtain ⟨m, ⟨i, f, hm⟩, hmin⟩ := Finset.wellFoundedLT.wf.has_min
    { s : Finset (F.obj j) | ∃ (i : _) (f : i ⟶ j), ↑s = range (F.map f) }
    ⟨_, i, hi, hf.coe_toFinset⟩

Goal state after:
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), ∃ i f, (range ⇑(ConcreteCategory.hom (F.map f))).Finite
j i✝ : J
hi : i✝ ⟶ j
hf : (range ⇑(ConcreteCategory.hom (F.map hi))).Finite
m : Finset (F.obj j)
hmin : ∀ x ∈ {s | ∃ i f, ↑s = range ⇑(ConcreteCategory.hom (F.map f))}, ¬x ⊂ m
i : J
f : i ⟶ j
hm : ↑m = range ⇑(ConcreteCategory.hom (F.map f))
⊢ ∃ i f, ∀ ⦃k : J⦄ (g : k ⟶ j), range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map g))
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✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
w : Fin (1 + 1) → R
hw : w 0 + w 1 = 1
h01 : ∀ (i : Fin (1 + 1)), w i ∈ Set.Ioo 0 1
i : Fin (1 + 1)
⊢ w i = Finset.affineCombinationLineMapWeights 0 1 (w 1) i

Tactic:
fin_cases i <;> simp [← hw]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h✝ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #{i | M i.1 i.2 ≠ 0} = m → ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
M : Matrix n n R
s : R
hs : 0 ≤ s
hM : ∃ M' ∈ doublyStochastic R n, M = s • M'
hd : #{i | M i.1 i.2 ≠ 0} = d
⊢ ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
rcases eq_or_lt_of_le hs with rfl | hs'

Goal state after:
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
h✝ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #{i | M i.1 i.2 ≠ 0} = m → ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
M : Matrix n n R
hd : #{i | M i.1 i.2 ≠ 0} = d
hs : 0 ≤ 0
hM : ∃ M' ∈ doublyStochastic R n, M = 0 • M'
⊢ ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M

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
h✝ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #{i | M i.1 i.2 ≠ 0} = m → ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
M : Matrix n n R
s : R
hs : 0 ≤ s
hM : ∃ M' ∈ doublyStochastic R n, M = s • M'
hd : #{i | M i.1 i.2 ≠ 0} = d
hs' : 0 < s
⊢ ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
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
⊢ {t | ↑t ⊆ s ∧ x ∈ (convexHull 𝕜) ↑t}.Nonempty

Tactic:
by
    simpa only [convexHull_eq_union_convexHull_finite_subsets s, exists_prop, mem_iUnion] using! hx

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
x y : P
⊢ Wbtw R y x ((pointReflection R x) y)

Tactic:
by
  refine ⟨2⁻¹, ⟨by simp, by norm_num⟩, ?_⟩
  rw [lineMap_apply, pointReflection_apply, vadd_vsub_assoc, ← two_smul R (x -ᵥ y)]
  simp

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

Goal state before:
pp: E : Type u_1
P : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
x z : P
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ dist x ((AffineMap.lineMap x z) a) + dist ((AffineMap.lineMap x z) a) z = dist x z

Tactic:
simp [abs_of_nonneg, ha₀, ha₁, sub_mul]

Goal state after:
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
hBA : B ⊆ A
hCB : C ⊆ B
⊢ IsExposed 𝕜 B C

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

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded ((-f) '' ball x₀ r)
⊢ ∃ K, LipschitzOnWith K f (ball x₀ r')

Tactic:
simpa using hf.neg.exists_lipschitzOnWith_of_isBounded hr hf'

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

Goal state before:
pp: R✝ : Type u_1
X : Type u_2
M✝ : Type u_3
N✝ : Type u_4
P✝ : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
N : Type u_10
P : Type u_11
w : StdSimplex R M
x✝ : M
inst✝ : IsStrictOrderedRing R
x y : M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
⊢ ((Finsupp.single x s + Finsupp.single y t).sum fun x r ↦ r) = 1

Tactic:
classical simpa [sum_add_index]

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

Goal state before:
pp: R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
inst✝ : IsStrictOrderedRing R
f : StdSimplex R (StdSimplex R (StdSimplex R M))
⊢ f.join.join = (map (fun x ↦ x.join) f).join

Tactic:
by
  ext1; simp [mapDomain, add_smul, sum_sum_index, sum_smul_index, smul_sum, mul_smul]

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

Goal state before:
pp: R : Type u_1
I : Type u_6
inst✝² : PartialOrder R
inst✝¹ : Semiring R
inst✝ : IsStrictOrderedRing R
w w' : StdSimplex R I
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
hst : s + t = 1
⊢ (convexCombPair s t hs ht hst w w').weights = s • w.weights + t • w'.weights

Tactic:
classical simp [convexCombPair, sum_add_index, add_smul]

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

Goal state before:
pp: case cons
K : Type u_4
X : Type u_5
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t✝ : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄, ↑t ⊆ s → t = w.weights.support → sConvexComb w ∈ s
w : StdSimplex K X
hw : ↑(Finset.cons x t hx) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
⊢ sConvexComb w ∈ s

Tactic:
| cons x t hx ht ih =>

Goal state after:
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.Ici e) f
hg : ConvexOn 𝕜 (Set.Iic e) g
h_mono : MonotoneOn f (Set.Ici e)
h_anti : AntitoneOn g (Set.Iic e)
h_eq : f e = g e
⊢ ConvexOn 𝕜 Set.univ ((Set.Ici e).piecewise f g)

Tactic:
have h_piecewise_Ici_eq_piecewise_Iic :
      (Set.Ici e).piecewise f g = (Set.Iic e).piecewise g f := by
    ext x; by_cases hx : x = e
      <;> simp [Set.piecewise, @le_iff_lt_or_eq _ _ x e, ← @ite_not _ (e ≤ _), hx, h_eq]
  rw [h_piecewise_Ici_eq_piecewise_Iic]
  exact convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici hg hf h_anti h_mono h_eq.symm

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow

Goal state before:
pp: case inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ ConcaveOn ℝ≥0 univ fun x ↦ x ^ p

Tactic:
rcases eq_or_lt_of_le hp₁ with (rfl | hp₁)

Goal state after:
case inr.inl
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ ConcaveOn ℝ≥0 univ fun x ↦ x ^ 1

case inr.inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁✝ : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ ConcaveOn ℝ≥0 univ fun x ↦ x ^ p
Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow

Goal state before:
pp: case inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ ConcaveOn ℝ (Ici 0) fun x ↦ x ^ p

Tactic:
rcases eq_or_lt_of_le hp₁ with (rfl | hp₁)

Goal state after:
case inr.inl
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ ConcaveOn ℝ (Ici 0) fun x ↦ x ^ 1

case inr.inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁✝ : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ ConcaveOn ℝ (Ici 0) fun x ↦ x ^ p
Module: Mathlib.Analysis.Convex.Strict.Extreme

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid A
inst✝¹ : Module 𝕜 A
inst✝ : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
x : A
hx : x ∈ C \ interior C
y : A
hy : y ∈ C
z : A
hz : z ∈ C
x✝ : x ∈ openSegment 𝕜 y z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxab : a • y + b • z = x
hyz : y = z
⊢ y = x

Tactic:
← hyz,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid A
inst✝¹ : Module 𝕜 A
inst✝ : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
x : A
hx : x ∈ C \ interior C
y : A
hy : y ∈ C
z : A
hz : z ∈ C
x✝ : x ∈ openSegment 𝕜 y z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxab : a • y + b • y = x
hyz : y = z
⊢ y = x
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ p₂ : P
m : V
c₁ c₂ : R
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h₁ : x -ᵥ p₁ = c₁ • m
h₂ : y -ᵥ p₂ = c₂ • m
hc : c₁ * c₂ ≤ 0
⊢ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
have h₂' : p₂ -ᵥ y = (-c₂) • m := by rw [← neg_vsub_eq_vsub_rev, h₂, neg_smul]

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ p₂ : P
m : V
c₁ c₂ : R
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h₁ : x -ᵥ p₁ = c₁ • m
h₂ : y -ᵥ p₂ = c₂ • m
hc : c₁ * c₂ ≤ 0
h₂' : p₂ -ᵥ y = -c₂ • m
⊢ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
h : s.SSameSide x y
ho : s.WOppSide x y
⊢ False

Tactic:
have hxy := wSameSide_and_wOppSide_iff.1 ⟨h.1, ho⟩

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
h : s.SSameSide x y
ho : s.WOppSide x y
hxy : x ∈ s ∨ y ∈ s
⊢ False
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
H1 : ¬BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
this✝ : ∀ (n : ℕ), g =ᵐ[volume.restrict (Ioc 0 ↑n)] 0
Hg : g =ᵐ[volume.restrict (⋃ n, Ioc 0 ↑n)] 0
this : ⋃ n, Ioc 0 ↑n = Ioi 0
⊢ g =ᵐ[volume.restrict (Ioi 0)] 0

Tactic:
rwa [this] at Hg

Goal state after:
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: D : Type u_4
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup D
inst✝ : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ : ∀ (N : ℕ), ∃ k C, ∃ (_ : 0 ≤ C), ∀ n ≤ N, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n g t x‖ ≤ C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ : ∀ n_1 ≤ n, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n_1 g t x‖ ≤ C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * ↑(k₂.choose k) * C₁ ^ k
x : D
hg' : ∀ i ≤ n, ‖iteratedFDerivWithin ℝ i g t (f x)‖ ≤ C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
i : ℕ
hi : 1 ≤ i
hi' : i ≤ n
⊢ C₁ * (1 + ‖x‖) ^ k₁ ≤ (1 + C₁) * (1 + ‖x‖) ^ k₁

Tactic:
gcongr; simp

Goal state after: