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

Goal state before:
pp: R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
l : List R
h : l.SortedLE
⊢ ∀ (i j k : ℕ) (hij : i < j) (hjk : j < k) (hk : k < l.length), Wbtw R l[i] l[j] l[k]

Tactic:
intro i j k hij hjk hk

Goal state after:
R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
l : List R
h : l.SortedLE
i j k : ℕ
hij : i < j
hjk : j < k
hk : k < l.length
⊢ Wbtw R l[i] l[j] l[k]
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: case inl
J : Type u
inst✝³ : Category.{w, u} J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this✝ : ∀ (i : J'), Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
h✝ : IsEmpty J
⊢ F.sections.Nonempty

pp: case inr
J : Type u
inst✝³ : Category.{w, u} J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this✝ : ∀ (i : J'), Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
h✝ : Nonempty J
⊢ F.sections.Nonempty

Tactic:
· fconstructor <;> apply isEmptyElim

Goal state after:
case inr
J : Type u
inst✝³ : Category.{w, u} J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this✝ : ∀ (i : J'), Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
h✝ : Nonempty J
⊢ F.sections.Nonempty
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case pos
𝕜 : 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 φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕' = ∅
hsφ : s.domRestrict φ = 0
⊢ ∃ 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:
have := congrFun hsφ
      refine ⟨fun _ => 0, fun _ => 0, ?_, ?_⟩
      · simp_all [domRestrict_def]
      · ext; simp_all

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

Goal state before:
pp: ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → ↥ι' → ↥(ι'.biUnion t) := fun f i ↦ ⟨↑f i, ⋯⟩
⊢ Finite ↑{f | Injective f ∧ ∀ (x : ↥ι'), f x ∈ t ↑x}

Tactic:
apply Finite.of_injective g

Goal state after:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → ↥ι' → ↥(ι'.biUnion t) := ⋯
⊢ Injective g
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
g : β ≃. γ
a : α
b : γ
⊢ (g.symm b).bind ⇑f.symm = some a ↔ (f a).bind ⇑g = some b

Tactic:
simp_all [and_comm, eq_some_iff f, eq_some_iff g, bind_eq_some_iff]

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

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ✝ τ✝ : Perm n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring R
σ τ : Perm n
⊢ Perm.permMatrix R (σ * τ)⁻¹ = Perm.permMatrix R σ⁻¹ * Perm.permMatrix R τ⁻¹

Tactic:
rw [_root_.mul_inv_rev, permMatrix_mul]

Goal state after:
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
hM : M ∈ rowStochastic R n
hx : ∀ (i : n), 0 ≤ x i
⊢ ∀ (j : n), 0 ≤ (x ᵥ* M) j

Tactic:
by
  intro j
  simp only [Matrix.vecMul, dotProduct]
  apply Finset.sum_nonneg
  intro k _
  apply mul_nonneg (hx k)
  exact nonneg_of_mem_rowStochastic hM

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

Goal state before:
pp: case mpr.inr
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
hs : 0 < s
⊢ ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s) →
    ∃ M' ∈ doublyStochastic R n, M = s • M'

Tactic:
rintro ⟨hM₁, hM₂, hM₃⟩

Goal state after:
case mpr.inr
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
hs : 0 < s
hM₁ : ∀ (i j : n), 0 ≤ M i j
hM₂ : ∀ (i : n), ∑ j, M i j = s
hM₃ : ∀ (j : n), ∑ i, M i j = s
⊢ ∃ M' ∈ doublyStochastic R n, M = s • 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
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
⊢ ∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = t.centerMass f id

Tactic:
let s := {z ∈ t | 0 < g z}

Goal state after:
𝕜 : Type u_1
E : Type u
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
⊢ ∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = t.centerMass f id
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 ∈ A.biUnion f, M i j ≤ ∑ i, ∑ j ∈ A.biUnion f, M i j

Tactic:
· exact sum_le_sum_of_subset_of_nonneg (by simp) fun _ _ _ => sum_nonneg fun j _ => hM.1 _ _

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

Goal state before:
pp: case refine_1
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : x ∈ ⋂ n, (1 + ↑(u n)) • ↑K
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
⊢ x ∈ ↑K

Tactic:
← K.isClosed.closure_eq,

Goal state after:
case refine_1
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : x ∈ ⋂ n, (1 + ↑(u n)) • ↑K
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑K
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 : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
hd : #{i | M i.1 i.2 ≠ 0} = d
hs'✝ : 0 < s
σ : Equiv.Perm n
hσ : ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
i : n
hi : i ∈ univ
hi' : ∀ x' ∈ univ, M i (σ i) ≤ M x' (σ x')
N : Matrix n n R := M - M i (σ i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i (σ i)
s' : R := s - M i (σ i)
hs' : 0 ≤ s'
this : ∃ M' ∈ doublyStochastic R n, N = s' • M'
⊢ #{i | N i.1 i.2 ≠ 0} < d

Tactic:
← hd

Goal state after:
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 : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
hd : #{i | M i.1 i.2 ≠ 0} = d
hs'✝ : 0 < s
σ : Equiv.Perm n
hσ : ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
i : n
hi : i ∈ univ
hi' : ∀ x' ∈ univ, M i (σ i) ≤ M x' (σ x')
N : Matrix n n R := M - M i (σ i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i (σ i)
s' : R := s - M i (σ i)
hs' : 0 ≤ s'
this : ∃ M' ∈ doublyStochastic R n, N = s' • M'
⊢ #{i | N i.1 i.2 ≠ 0} < #{i | M i.1 i.2 ≠ 0}
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
⊢ Set.extremePoints R ↑(doublyStochastic R n) = {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

Tactic:
by
  refine subset_antisymm ?_ ?_
  · rw [doublyStochastic_eq_convexHull_permMatrix]
    exact extremePoints_convexHull_subset
  rintro _ ⟨σ, rfl⟩
  refine ⟨permMatrix_mem_doublyStochastic, fun x₁ hx₁ x₂ hx₂ hσ ↦ ?_⟩
  suffices ∀ i j : n, x₁ i j = x₂ i j by
    obtain rfl : x₁ = x₂ := by simpa [← Matrix.ext_iff]
    simp_all
  intro i j
  have h₁ : σ.permMatrix R i j ∈ openSegment R (x₁ i j) (x₂ i j) :=
    image_openSegment _ (entryLinearMap R R i j).toAffineMap x₁ x₂ ▸ ⟨_, hσ, rfl⟩
  by_contra! h
  have h₂ : openSegment R (x₁ i j) (x₂ i j) ⊆ Set.Ioo 0 1 := by
    rw [openSegment_eq_Ioo' h]
    apply Set.Ioo_subset_Ioo <;>
    simp_all [nonneg_of_mem_doublyStochastic, le_one_of_mem_doublyStochastic]
  specialize h₂ h₁
  aesop

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
⊢ dual p ↑(hull R s) = dual p s

Tactic:
refine le_antisymm (dual_anti Submodule.subset_span) (fun x hx y hy => ?_)
  induction hy using Submodule.span_induction with
  | mem _y h => exact hx h
  | zero => simp
  | add y z _hy _hz hy hz => rw [map_add, add_apply]; exact add_nonneg hy hz
  | smul t y _hy hy => rw [map_smul_of_tower, Nonneg.mk_smul, smul_apply]; exact mul_nonneg t.2 hy

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
hull_sub_span : ↑(hull ℝ s) ⊆ ↑(Submodule.span ℝ s)
b : Basis ↑s ℝ E := Basis.mk hs_lin ⋯
h_coord_dual : ∀ (i : ↑s), b.coord i ∈ dual (Dual.eval ℝ E) ↑C₁
z : E ⊗[ℝ] F
hz : z ∈ C₁.maxTensorProduct ↑C₂
⊢ z ∈ C₁.minTensorProduct ↑C₂

Tactic:
← (equivFinsuppOfBasisLeft b).symm_apply_apply z,

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
hull_sub_span : ↑(hull ℝ s) ⊆ ↑(Submodule.span ℝ s)
b : Basis ↑s ℝ E := Basis.mk hs_lin ⋯
h_coord_dual : ∀ (i : ↑s), b.coord i ∈ dual (Dual.eval ℝ E) ↑C₁
z : E ⊗[ℝ] F
hz : z ∈ C₁.maxTensorProduct ↑C₂
⊢ (equivFinsuppOfBasisLeft b).symm ((equivFinsuppOfBasisLeft b) z) ∈ C₁.minTensorProduct ↑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
⊢ B ⊆ A

Tactic:
rintro x hx
  obtain ⟨_, rfl⟩ := hAB ⟨x, hx⟩
  exact hx.1

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

Goal state before:
pp: β : Type u_2
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsLocalMinOn f (Icc a b) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
⊢ f a ≤ f c

Tactic:
rw [IsLocalMinOn, nhdsWithin_Icc_eq_nhdsGE a_lt_b] at h_local_min

Goal state after:
β : Type u_2
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
⊢ f a ≤ f c
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 - ε)
⊢ f x - f y ≤ K * ‖x - y‖

Tactic:
obtain rfl | hxy := eq_or_ne x y

Goal state after:
case inl
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 : E
hx hy : x ∈ ball x₀ (r - ε)
⊢ f x - f x ≤ K * ‖x - x‖

case inr
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 - ε)
hxy : x ≠ y
⊢ f x - f y ≤ K * ‖x - y‖
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hc : ∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t
t : Set { x // x ∈ s }
x : { x // x ∈ s }
h : ↑x ∈ (convexHull 𝕜) (Subtype.val '' t)
⊢ x ∈ t

Tactic:
← Subtype.coe_injective.mem_set_image

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hc : ∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t
t : Set { x // x ∈ s }
x : { x // x ∈ s }
h : ↑x ∈ (convexHull 𝕜) (Subtype.val '' t)
⊢ ↑x ∈ (fun a ↦ ↑a) '' t
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]

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.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
h_piecewise_Ici_eq_piecewise_Iic : (Set.Ici e).piecewise f g = (Set.Iic e).piecewise g f
⊢ ConvexOn 𝕜 Set.univ ((Set.Ici e).piecewise f g)
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) ≤ |s - s'| * dist x y

Tactic:
convert dist_iConvexComb_le f ![x, x, y] ![x, y, y] using 1

Goal state after:
case e'_3
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) =
    dist (iConvexComb f ![x, x, y]) (iConvexComb f ![x, y, y])

case e'_4
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
⊢ |s - s'| * dist x y = iConvexComb f fun i ↦ dist (![x, x, y] i) (![x, y, y] i)
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G ≠ ⊤ ↔ ∃ a b, a ≠ b ∧ ¬G.Adj a b

Tactic:
by
  simp [eq_top_iff_forall_ne_adj]

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : Set (Set E)
h_card : ↑(finrank 𝕜 E) + 1 ≤ F.encard
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → #G = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
I : Finset (Set E)
hI_ss : ↑I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Set (Set E)
left✝ : ↑I ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = ↑(finrank 𝕜 E) + 1
hJ_fin : Fintype ↑J
J' : Finset (Set E) := J.toFinset
⊢ (⋂₀ J).Nonempty

Tactic:
← coe_toFinset J

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : Set (Set E)
h_card : ↑(finrank 𝕜 E) + 1 ≤ F.encard
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → #G = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
I : Finset (Set E)
hI_ss : ↑I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Set (Set E)
left✝ : ↑I ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = ↑(finrank 𝕜 E) + 1
hJ_fin : Fintype ↑J
J' : Finset (Set E) := J.toFinset
⊢ (⋂₀ ↑J.toFinset).Nonempty
Module: Mathlib.Analysis.Convex.Strict.Extreme

Goal state before:
pp: A : Type u_1
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace ℝ A
inst✝¹ : Nontrivial A
x : A
r : ℝ
inst✝ : StrictConvexSpace ℝ A
⊢ closedBall x r \ interior (closedBall x r) = sphere x r

Tactic:
interior_closedBall',

Goal state after:
A : Type u_1
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace ℝ A
inst✝¹ : Nontrivial A
x : A
r : ℝ
inst✝ : StrictConvexSpace ℝ A
⊢ closedBall x r \ ball x r = sphere x r
Module: Mathlib.Analysis.Convex.StoneSeparation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q u v x y z : E
hz : z ∈ segment 𝕜 x y
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
⊢ ¬Disjoint (segment 𝕜 u v) ((convexHull 𝕜) {p, q, z})

Tactic:
not_disjoint_iff

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q u v x y z : E
hz : z ∈ segment 𝕜 x y
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
⊢ ∃ x ∈ segment 𝕜 u v, x ∈ (convexHull 𝕜) {p, q, z}
Module: Mathlib.Analysis.Convex.StoneSeparation

Goal state before:
pp: case inr.inr.refine_3
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
⊢ az * av / (az * av + bz * au) + bz * au / (az * av + bz * au) = 1

Tactic:
rw [← add_div, div_self]; positivity

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

Goal state before:
pp: case mp.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
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
hy : y ∈ s
⊢ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

pp: case mp.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
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
p : P
hp : p ∈ s
hr : SameRay R (y -ᵥ p₂) (p -ᵥ x)
⊢ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
· exact Or.inl hy

Goal state after:
case mp.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
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
p : P
hp : p ∈ s
hr : SameRay R (y -ᵥ p₂) (p -ᵥ x)
⊢ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mpr.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
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
hy : y ∈ s
⊢ y ∈ s ∨ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ x)

pp: case mpr.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
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
p : P
hp : p ∈ s
hr : SameRay R (x -ᵥ p) (p₂ -ᵥ y)
⊢ y ∈ s ∨ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ x)

Tactic:
· exact Or.inl hy

Goal state after:
case mpr.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
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
p : P
hp : p ∈ s
hr : SameRay R (x -ᵥ p) (p₂ -ᵥ y)
⊢ y ∈ s ∨ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ x)