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

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ ∅ = {x | x ∈ A ∧ 1 ≤ 0 x}

Tactic:
rw [eq_comm, eq_empty_iff_forall_notMem]

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ ∀ (x : E), x ∉ {x | x ∈ A ∧ 1 ≤ 0 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
hsc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) '' closure[inst✝³] s = closure[inst✝³] t

Tactic:
refine Subset.antisymm (mapsTo_gaugeRescale_closure hsc hs₀ htc
    (mem_of_mem_nhds ht₀) (absorbent_nhds_zero ht₀)).image_subset ?_

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
hs₀ : s ∈ 𝓝 0
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ closure[inst✝³] t ⊆ ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) '' closure[inst✝³] s
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
a b : ι
hab : p a = p b
⊢ p a ∈ (convexHull 𝕜) ↑(image p {b})

Tactic:
rw [hab, image_singleton, coe_singleton, convexHull_singleton]

Goal state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
a b : ι
hab : p a = p b
⊢ p b ∈ {p b}
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
hxyz : x = a • y + b • z
⊢ ‖x - y‖ * (f z - f x) ≤ ‖x - y‖ * (2 * M)

Tactic:
by
        rw [sub_eq_add_neg (f _), two_mul]
        gcongr
        · exact (le_abs_self _).trans <| hM _ hz
        · exact (neg_le_abs _).trans <| hM _ hx'

Goal state after:
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
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ y +ᵥ ⇑h '' closure[inst✝³] (-x +ᵥ s) = closure[inst✝³] t

Tactic:
image_gaugeRescaleHomeomorph_closure,

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) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ y +ᵥ closure[inst✝³] (-y +ᵥ t) = closure[inst✝³] t
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
⊢ ∀ (a : E), dist a x₀ < r → |(-f) a| ≤ M

Tactic:
simpa using hM

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

Goal state before:
pp: case refine_3
α : 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
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto (fun n ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
⊢ ∀ i ∈ (G n).range, ↑(ContinuousLinearMap.id ℝ E) i ∈ s

Tactic:
· simp only [SimpleFunc.mem_range, forall_mem_range]
    intro x
    apply (range g).inter_subset_right
    exact SimpleFunc.approxOn_mem hgm.measurable h₀ _ _

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

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
inst✝ : IsFiniteMeasure μ
hfi : Integrable f μ
H : ∀ (t : Set α), MeasurableSet t → μ t ≠ 0 → μ tᶜ ≠ 0 → ⨍ (x : α) in t, f x ∂μ = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ¬μ t = 0
h₀' : t =ᵐ[μ] univ
⊢ ∫ (x : α), f x ∂μ = μ.real t • ⨍ (x : α), f x ∂μ

Tactic:
measureReal_congr h₀',

Goal state after:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
inst✝ : IsFiniteMeasure μ
hfi : Integrable f μ
H : ∀ (t : Set α), MeasurableSet t → μ t ≠ 0 → μ tᶜ ≠ 0 → ⨍ (x : α) in t, f x ∂μ = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ¬μ t = 0
h₀' : t =ᵐ[μ] univ
⊢ ∫ (x : α), f x ∂μ = μ.real univ • ⨍ (x : α), f x ∂μ
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : ↥(affineSpan 𝕜 s)
h : ∀ (o : Set ↥(affineSpan 𝕜 s)), IsOpen[instTopologicalSpaceSubtype] o → x ∈ o → (o ∩ Subtype.val ⁻¹' s).Nonempty
t : Set P
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hx : ↑x ∈ t
⊢ (t ∩ s).Nonempty

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := h _ (continuous_induced_dom.isOpen_preimage t ht) hx

Goal state after:
case refine_1
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : ↥(affineSpan 𝕜 s)
h : ∀ (o : Set ↥(affineSpan 𝕜 s)), IsOpen[instTopologicalSpaceSubtype] o → x ∈ o → (o ∩ Subtype.val ⁻¹' s).Nonempty
t : Set P
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hx : ↑x ∈ t
z : ↥(affineSpan 𝕜 s)
hz₁ : z ∈ Subtype.val ⁻¹' t
hz₂ : z ∈ Subtype.val ⁻¹' s
⊢ (t ∩ s).Nonempty
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

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

Tactic:
by
  ext a; by_cases x = a <;> simp [*, mapDomain]

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
J₁ : Type u₁
J₂ : Type u₂
g₁ : StdSimplex R J₁
g₂ : StdSimplex R J₂
m₁ : J₁ → M
m₂ : J₂ → M
this :
  (iConvexComb (duple 0 1 hs ht h) fun i ↦
      iConvexComb (Fin.cons (map ULift.up g₁) (Fin.cons (map ULift.up g₂) fun a ↦ nomatch a) i)
        (Fin.cons (m₁ ∘ ULift.down) (Fin.cons (m₂ ∘ ULift.down) fun a a_1 ↦ nomatch a, a_1) i)) =
    iConvexComb
      (iConvexComb (duple 0 1 hs ht h) fun i ↦
        map (fun x ↦ ⟨i, x⟩) (Fin.cons (map ULift.up g₁) (Fin.cons (map ULift.up g₂) fun a ↦ nomatch a) i))
      (Sigma.uncurry (Fin.cons (m₁ ∘ ULift.down) (Fin.cons (m₂ ∘ ULift.down) fun a a_1 ↦ nomatch a, a_1)))
⊢ convexCombPair s t hs ht h (iConvexComb g₁ m₁) (iConvexComb g₂ m₂) =
    sConvexComb (convexCombPair s t hs ht h (map m₁ g₁) (map m₂ g₂))

Tactic:
simp [iConvexComb, map_sConvexComb, map_map, Sigma.uncurry] at this

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
J₁ : Type u₁
J₂ : Type u₂
g₁ : StdSimplex R J₁
g₂ : StdSimplex R J₂
m₁ : J₁ → M
m₂ : J₂ → M
this :
  sConvexComb (duple (sConvexComb (map (fun x ↦ m₁ x) g₁)) (sConvexComb (map (fun x ↦ m₂ x) g₂)) hs ht h) =
    sConvexComb (sConvexComb (duple (map (fun x ↦ m₁ x) g₁) (map (fun x ↦ m₂ x) g₂) hs ht h))
⊢ convexCombPair s t hs ht h (iConvexComb g₁ m₁) (iConvexComb g₂ m₂) =
    sConvexComb (convexCombPair s t hs ht h (map m₁ g₁) (map m₂ g₂))
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: ι : Type u_1
R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R ι
f : ι → X
hf : ∀ (i : ι), w.weights i ≠ 0 → f i ∈ s
⊢ iConvexComb w f ∈ s

Tactic:
classical
  refine hs ?_
  grw [StdSimplex.weights_map, mapDomain_support]
  simpa [subset_def]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
X : ι → Type u_7
inst✝ : (i : ι) → ConvexSpace R (X i)
s : Set ι
t : (i : ι) → Set (X i)
ht : ∀ i ∈ s, IsConvexSet R (t i)
⊢ IsConvexSet R (s.pi t)

Tactic:
refine fun w hw i hi ↦ ht i hi ?_

Goal state after:
ι : Type u_1
R : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
X : ι → Type u_7
inst✝ : (i : ι) → ConvexSpace R (X i)
s : Set ι
t : (i : ι) → Set (X i)
ht : ∀ i ∈ s, IsConvexSet R (t i)
w : StdSimplex R ((i : ι) → X i)
hw : ↑w.weights.support ⊆ s.pi t
i : ι
hi : i ∈ s
⊢ ↑(StdSimplex.map (fun x ↦ x i) w).weights.support ⊆ t i
Module: Mathlib.Analysis.Convex.Quasiconvex

Goal state before:
pp: case inr
𝕜 : Type u_4
E : Type u_5
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_6
γ : Type u_7
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
this :
  ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
    [inst_3 : SMul 𝕜 E] {β : Type u_6} {γ : Type u_7} [inst_4 : LinearOrder β] [inst_5 : Preorder γ] {s : Set E}
    {f : E → β} {g : β → γ},
    Monotone g →
      QuasiconvexOn 𝕜 s f →
        ∀ (c : γ) (x : E),
          x ∈ s ∧ g (f x) ≤ c →
            ∀ (y : E),
              y ∈ s ∧ g (f y) ≤ c →
                ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f x ≤ f y → a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
h : ¬f x ≤ f y
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c

pp: 𝕜✝ : Type u_4
E✝ : Type u_5
inst✝¹¹ : Semiring 𝕜✝
inst✝¹⁰ : PartialOrder 𝕜✝
inst✝⁹ : AddCommMonoid E✝
inst✝⁸ : SMul 𝕜✝ E✝
β✝ : Type u_6
γ✝ : Type u_7
inst✝⁷ : LinearOrder β✝
inst✝⁶ : Preorder γ✝
s✝ : Set E✝
f✝ : E✝ → β✝
g✝ : β✝ → γ✝
𝕜 : Type u_4
E : Type u_5
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_6
γ : Type u_7
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f x ≤ f y
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c

Tactic:
· grind

Goal state after:
𝕜✝ : Type u_4
E✝ : Type u_5
inst✝¹¹ : Semiring 𝕜✝
inst✝¹⁰ : PartialOrder 𝕜✝
inst✝⁹ : AddCommMonoid E✝
inst✝⁸ : SMul 𝕜✝ E✝
β✝ : Type u_6
γ✝ : Type u_7
inst✝⁷ : LinearOrder β✝
inst✝⁶ : Preorder γ✝
s✝ : Set E✝
f✝ : E✝ → β✝
g✝ : β✝ → γ✝
𝕜 : Type u_4
E : Type u_5
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_6
γ : Type u_7
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f x ≤ f y
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: case inr.succ
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : ↥s → E := fun i ↦ ⋯.some
⊢ (⋂ i ∈ s, F i).Nonempty

Tactic:
have h_ind : ¬AffineIndependent 𝕜 a := by
    rw [← finrank_vectorSpan_le_iff_not_affineIndependent 𝕜 a (n := (k - 1))]
    · exact (Submodule.finrank_le (vectorSpan 𝕜 (range a))).trans (Nat.le_pred_of_lt h_card)
    · simp only [card_coe]; lia

Goal state after:
case inr.succ
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : ↥s → E := fun i ↦ ⋯.some
h_ind : ¬AffineIndependent 𝕜 a
⊢ (⋂ i ∈ s, F i).Nonempty
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: case h.h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : ↥s → E := ⋯
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i : ↥s
J : Set ↥s
hi : i ∈ J
v : E
j : ↥s
hj : j ∈ Jᶜ
hj_v : a j = v
⊢ ⋂ k ∈ s.erase ↑j, F k ⊆ F ↑i

pp: case h.a
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : ↥s → E := ⋯
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i : ↥s
J : Set ↥s
hi : i ∈ J
v : E
j : ↥s
hj : j ∈ Jᶜ
hj_v : a j = v
⊢ a j ∈ ⋂ k ∈ s.erase ↑j, F k

Tactic:
· apply iInter₂_subset
    simp [mem_erase, ne_of_mem_of_not_mem hi hj]

Goal state after:
case h.a
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : ↥s → E := ⋯
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i : ↥s
J : Set ↥s
hi : i ∈ J
v : E
j : ↥s
hj : j ∈ Jᶜ
hj_v : a j = v
⊢ a j ∈ ⋂ k ∈ s.erase ↑j, F k
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint G.edgeSet (fromEdgeSet s).edgeSet ↔ Disjoint G.edgeSet (s \ Sym2.diagSet ∪ s ∩ Sym2.diagSet)

Tactic:
edgeSet_fromEdgeSet

Goal state after:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint G.edgeSet (s \ Sym2.diagSet) ↔ Disjoint G.edgeSet (s \ Sym2.diagSet ∪ s ∩ Sym2.diagSet)
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: case inr.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ = p₃
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)

Tactic:
exact False.elim (hp₂p₃ h)

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

Goal state before:
pp: case pos
R : Type u_1
V : Type u_2
ι : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi✝ : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬∑ j ∈ t, w j = 0
hi : ¬w i = 0
hzi : z i = t.centerMass w z
hwi : w i + ∑ j ∈ t, w j ≠ 0
hijt : ∃ i'' j'', i'' ∈ t ∧ j'' ∈ t ∧ z i'' ≠ z j'' ∧ w i'' ≠ 0 ∧ w j'' ≠ 0
⊢ t.centerMass w z ∈ interior s

pp: case neg
R : Type u_1
V : Type u_2
ι : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi✝ : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬∑ j ∈ t, w j = 0
hi : ¬w i = 0
hzi : z i = t.centerMass w z
hwi : w i + ∑ j ∈ t, w j ≠ 0
hijt : ∀ (i'' j'' : ι), i'' ∈ t → j'' ∈ t → z i'' ≠ z j'' → w i'' ≠ 0 → w j'' = 0
⊢ t.centerMass w z ∈ interior s

Tactic:
· grind

Goal state after:
case neg
R : Type u_1
V : Type u_2
ι : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi✝ : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬∑ j ∈ t, w j = 0
hi : ¬w i = 0
hzi : z i = t.centerMass w z
hwi : w i + ∑ j ∈ t, w j ≠ 0
hijt : ∀ (i'' j'' : ι), i'' ∈ t → j'' ∈ t → z i'' ≠ z j'' → w i'' ≠ 0 → w j'' = 0
⊢ t.centerMass w z ∈ interior s
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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
⊢ (r₂ / (r₁ + r₂)) • (-(p₂ -ᵥ y) + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) = (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁)

Tactic:
linear_combination (norm := match_scalars <;> field) (r₁ + r₂)⁻¹ • h

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
a b m : ℝ
x y : E
f : E → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * (f x - m / 2 * ‖x‖ ^ 2) + b * (f y - m / 2 * ‖y‖ ^ 2) +
      m / 2 * ((a * ‖x‖) ^ 2 + 2 * (a * (b * inner ℝ x y)) + (‖b‖ * ‖y‖) ^ 2) =
    a * f x + b * f y - m / 2 * a * b * (‖x‖ ^ 2 - 2 * inner ℝ x y + ‖y‖ ^ 2)

Tactic:
norm_of_nonneg hb,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
a b m : ℝ
x y : E
f : E → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * (f x - m / 2 * ‖x‖ ^ 2) + b * (f y - m / 2 * ‖y‖ ^ 2) +
      m / 2 * ((a * ‖x‖) ^ 2 + 2 * (a * (b * inner ℝ x y)) + (b * ‖y‖) ^ 2) =
    a * f x + b * f y - m / 2 * a * b * (‖x‖ ^ 2 - 2 * inner ℝ x y + ‖y‖ ^ 2)
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case h
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : ℕ → ℕ
hk : ∀ (n : ℕ), iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k n
n : ℕ
hn : n ≤ N
⊢ iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ (Finset.range (N + 1)).sup k

Tactic:
refine (hk n).trans (isBigO_of_le _ fun x ↦ ?_)

Goal state after:
case h
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : ℕ → ℕ
hk : ∀ (n : ℕ), iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k n
n : ℕ
hn : n ≤ N
x : E
⊢ ‖(1 + ‖x‖) ^ k n‖ ≤ ‖(1 + ‖x‖) ^ (Finset.range (N + 1)).sup k‖