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

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
s : R
hs : 0 ≤ s
M' : Matrix n n R
hM' : M' ∈ doublyStochastic R n
⊢ (∀ (i j : n), 0 ≤ (s • M') i j) ∧ (∀ (i : n), ∑ j, (s • M') i j = s) ∧ ∀ (j : n), ∑ i, (s • M') i j = s

Tactic:
rw [mem_doublyStochastic_iff_sum] at hM'

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
s : R
hs : 0 ≤ s
M' : Matrix n n R
hM' : (∀ (i j : n), 0 ≤ M' i j) ∧ (∀ (i : n), ∑ j, M' i j = 1) ∧ ∀ (j : n), ∑ i, M' i j = 1
⊢ (∀ (i j : n), 0 ≤ (s • M') i j) ∧ (∀ (i : n), ∑ j, (s • M') i j = s) ∧ ∀ (j : n), ∑ i, (s • M') i j = s
Module: Mathlib.Analysis.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁹ : AddCommMonoid E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Semifield 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : DenselyOrdered 𝕜
inst✝¹ : NoMaxOrder 𝕜
inst✝ : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hSclos : IsClosed ↑C
x : E
hx : x ∈ ↑C
⊢ C.Pointed

Tactic:
let f : 𝕜 → E := (· • x)

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁹ : AddCommMonoid E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Semifield 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : DenselyOrdered 𝕜
inst✝¹ : NoMaxOrder 𝕜
inst✝ : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hSclos : IsClosed ↑C
x : E
hx : x ∈ ↑C
f : 𝕜 → E := fun x_1 ↦ x_1 • x
⊢ C.Pointed
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_2.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 y : P
r : R
hr : 1 ≤ r
⊢ (r⁻¹ * r) • (y -ᵥ x) +ᵥ x = y

Tactic:
inv_mul_cancel₀ (one_pos.trans_le hr).ne',

Goal state after:
case refine_2.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 y : P
r : R
hr : 1 ≤ r
⊢ 1 • (y -ᵥ x) +ᵥ x = y
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
⊢ ↑(doublyStochastic R n) = (convexHull R) {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

Tactic:
refine (convexHull_min ?g1 convex_doublyStochastic).antisymm' fun M hM => ?g2

Goal state after:
case g1
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
⊢ {x | ∃ σ, Equiv.Perm.permMatrix R σ = x} ⊆ ↑(doublyStochastic R n)

case g2
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)
⊢ M ∈ (convexHull R) {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}
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✝ t : Set M
y✝ : N
s : Set M
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : N
hy : y ∈ {y | ∀ ⦃x : M⦄, x ∈ s → 0 ≤ (p x) y}
x : M
hx : x ∈ s
⊢ 0 ≤ (p x) (c • y)

Tactic:
← Nonneg.coe_smul,

Goal state after:
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✝ t : Set M
y✝ : N
s : Set M
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : N
hy : y ∈ {y | ∀ ⦃x : M⦄, x ∈ s → 0 ≤ (p x) y}
x : M
hx : x ∈ s
⊢ 0 ≤ (p x) (↑c • y)
Module: Mathlib.Analysis.Convex.Cone.TensorProduct

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_3
b : Basis ι R M
C : PointedCone R M
hC : ↑C ⊆ ↑(hull R (Set.range ⇑b))
i : ι
⊢ b.coord i ∈ dual (Dual.eval R M) ↑C

Tactic:
classical
  refine dual_le_dual hC ?_
  simp [Finsupp.single_apply, ite_nonneg zero_le_one le_rfl]

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

Goal state before:
pp: case refine_2
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
i : ↑s
x✝ : i ∈ Finset.univ
f : F →L[ℝ] ℝ
hf : ↑f ∈ dual (Dual.eval ℝ F) ↑C₂
hz : ∀ φ ∈ dual (Dual.eval ℝ E) ↑C₁, ∀ ψ ∈ dual (Dual.eval ℝ F) ↑↑C₂, 0 ≤ ((dualDistrib ℝ E F) (φ ⊗ₜ[ℝ] ψ)) z
h_nonneg : 0 ≤ ((dualDistrib ℝ E F) (b.coord i ⊗ₜ[ℝ] ↑f)) z
⊢ 0 ≤ ((topDualPairing ℝ F) f) ((TensorProduct.lid ℝ F) ((LinearMap.rTensor F (b.coord i)) z))

Tactic:
have h_eq : dualDistrib ℝ E F ((b.coord i) ⊗ₜ[ℝ] (f : F →ₗ[ℝ] ℝ)) =
        (f : F →ₗ[ℝ] ℝ) ∘ₗ (TensorProduct.lid ℝ F) ∘ₗ (b.coord i).rTensor F := by
      ext; simp [mul_comm]

Goal state after:
case refine_2
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
i : ↑s
x✝ : i ∈ Finset.univ
f : F →L[ℝ] ℝ
hf : ↑f ∈ dual (Dual.eval ℝ F) ↑C₂
hz : ∀ φ ∈ dual (Dual.eval ℝ E) ↑C₁, ∀ ψ ∈ dual (Dual.eval ℝ F) ↑↑C₂, 0 ≤ ((dualDistrib ℝ E F) (φ ⊗ₜ[ℝ] ψ)) z
h_nonneg : 0 ≤ ((dualDistrib ℝ E F) (b.coord i ⊗ₜ[ℝ] ↑f)) z
h_eq : (dualDistrib ℝ E F) (b.coord i ⊗ₜ[ℝ] ↑f) = ↑f ∘ₗ ↑(TensorProduct.lid ℝ F) ∘ₗ LinearMap.rTensor F (b.coord i)
⊢ 0 ≤ ((topDualPairing ℝ F) f) ((TensorProduct.lid ℝ F) ((LinearMap.rTensor F (b.coord i)) z))
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
x : E
hx : gauge t x ≠ 0
⊢ gauge s x / gauge t x * gauge t x = gauge s x

Tactic:
div_mul_cancel₀ _ hx

Goal state after:
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
x : E
hx : gauge t x ≠ 0
⊢ gauge s x = gauge s x
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
A : Set E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : ContinuousAdd 𝕜
F : Finset (Set E)
hF : F.Nonempty
hAF : ∀ B ∈ F, IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (⋂₀ ↑F)

Tactic:
by
  induction F using Finset.induction with
  | empty => exfalso; exact Finset.not_nonempty_empty hF
  | insert C F _ hF' =>
    rw [Finset.coe_insert, sInter_insert]
    obtain rfl | hFnemp := F.eq_empty_or_nonempty
    · rw [Finset.coe_empty, sInter_empty, inter_univ]
      exact hAF C (Finset.mem_singleton_self C)
    · exact (hAF C (Finset.mem_insert_self C F)).inter
        (hF' hFnemp fun B hB => hAF B (Finset.mem_insert_of_mem hB))

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
⊢ intrinsicFrontier 𝕜 s ∪ intrinsicInterior 𝕜 s = intrinsicClosure 𝕜 s

Tactic:
by
  rw [union_comm, intrinsicInterior_union_intrinsicFrontier]

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

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

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

Tactic:
←
    AffineIsometryEquiv.coe_toAffineEquiv,

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

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

Goal state before:
pp: R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
y : Y
⊢ (StdSimplex.map f
          { weights := onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) ⋯, nonneg := ⋯, total := ⋯ }).weights
      y =
    w.weights y

Tactic:
StdSimplex.weights_map

Goal state after:
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
y : Y
⊢ (mapDomain f
        { weights := onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) ⋯, nonneg := ⋯, total := ⋯ }.weights)
      y =
    w.weights y
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
⊢ IsConvexSet R (f '' s)

Tactic:
by
  classical
  rintro w hw
  obtain ⟨u, hus, hfu, huw⟩ := Finset.exists_subset_injOn_image_eq_of_surjOn _ _ hw
  refine ⟨sConvexComb {
      weights := .onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) <| by simp +contextual
      nonneg x := by simp; split <;> simp
      total := by
        simp only [implies_true, sum_onFinset, Finset.sum_ite_mem, Finset.inter_self,
        ← Finset.sum_image hfu, huw]
        exact w.total
    }, hs.sConvexComb_mem <| by grw [support_onFinset_subset, hus], ?_⟩
  rw [hf.map_sConvexComb]
  congr
  ext y
  rw [StdSimplex.weights_map]
  by_cases hy : y ∈ w.weights.support
  · rw [← huw, Finset.mem_image] at hy
    obtain ⟨x, hx, rfl⟩ := hy
    convert mapDomain_apply' _ _ support_onFinset_subset hfu hx
    exact (if_pos hx).symm
  · rw [mapDomain_of_not_mem_image_support (by simp [← huw] at ⊢ hy; tauto)]
    simp_all

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
x : E
⊢ (Set.Ici e).piecewise f g x = (Set.Iic e).piecewise g f x

Tactic:
by_cases hx : x = e

Goal state after:
case pos
𝕜 : 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
x : E
hx : x = e
⊢ (Set.Ici e).piecewise f g x = (Set.Iic e).piecewise g f x

case neg
𝕜 : 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
x : E
hx : ¬x = e
⊢ (Set.Ici e).piecewise f g x = (Set.Iic e).piecewise g f x
Module: Mathlib.Analysis.Convex.MetricSpace

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

Tactic:
obtain ht | ht : f t = 0 ∨ f t = 1 := by
    simpa [le_antisymm_iff, hf0, hf1, -not_and, not_and_or] using ht

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

case neg.inr
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
⊢ ContinuousAt (fun i ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) t
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
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ (⋂₀ ↑F).Nonempty

Tactic:
classical -- for DecidableEq, required for the family version
  rw [show ⋂₀ F = ⋂ X ∈ F, (X : Set E) by ext; simp]
  apply helly_theorem' h_convex
  intro G hG_ss hG_card
  rw [show ⋂ X ∈ G, X = ⋂₀ G by ext; simp]
  exact h_inter G hG_ss hG_card

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

Goal state before:
pp: ι : Sort u_1
V : Type u
G H : SimpleGraph V
a b c u v w : V
e : Sym2 V
G₁ G₂ : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ Fintype ↑(G₁ \ G₂).edgeSet

Tactic:
rw [edgeSet_sdiff]
  exact Set.fintypeDiff _ _

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
hv : v ∈ e
⊢ G.otherVertexOfIncident ⋯ ∈ G.neighborSet v

Tactic:
← Sym2.other_spec' hv,

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v : V
e : Sym2 V
he✝ : e ∈ G.edgeSet
hv : v ∈ e
he : s(v, Sym2.Mem.other' hv) ∈ G.edgeSet
⊢ G.otherVertexOfIncident ⋯ ∈ G.neighborSet v
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: case pos
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
h : Wbtw ℝ p₁ p₂ p₃
hp₁ : ¬p₂ = p₁
hp₃ : p₂ = p₃
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)

Tactic:
simp [hp₃]

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

Goal state before:
pp: case pos
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
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : p₁ = p₂
⊢ Wbtw ℝ p₁ p₂ p₃

pp: case neg
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
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : ¬p₁ = p₂
⊢ Wbtw ℝ p₁ p₂ p₃

Tactic:
· simp [hp₁p₂]

Goal state after:
case neg
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
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : ¬p₁ = p₂
⊢ Wbtw ℝ p₁ p₂ p₃
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 z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (z -ᵥ p₃)
⊢ s.WSameSide x z

Tactic:
refine ⟨p₁, hp₁, p₃, hp₃, hxy.trans hyz ?_⟩

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 z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (z -ᵥ p₃)
⊢ y -ᵥ p₂ = 0 → x -ᵥ p₁ = 0 ∨ z -ᵥ p₃ = 0
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 z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)
⊢ s.WOppSide x z

Tactic:
refine ⟨p₁, hp₁, p₃, hp₃, hxy.trans hyz ?_⟩

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 z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)
⊢ y -ᵥ p₂ = 0 → x -ᵥ p₁ = 0 ∨ p₃ -ᵥ z = 0
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 z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)
⊢ s.WSameSide x z

Tactic:
refine ⟨p₁, hp₁, p₃, hp₃, hxy.trans hyz ?_⟩

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 z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)
⊢ p₂ -ᵥ y = 0 → x -ᵥ p₁ = 0 ∨ z -ᵥ p₃ = 0
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case inr.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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
⊢ ∃ p ∈ s, Wbtw R x p y

Tactic:
refine ⟨lineMap x y (r₂ / (r₁ + r₂)), ?_, ?_⟩

Goal state after:
case inr.inr.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
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)
⊢ (lineMap x y) (r₂ / (r₁ + r₂)) ∈ s

case inr.inr.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
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)
⊢ Wbtw R x ((lineMap x y) (r₂ / (r₁ + r₂))) y
Module: Mathlib.Analysis.Convex.Strong

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
⊢ StrongConvexOn s m f ↔ ConvexOn ℝ s fun x ↦ f x - m / 2 * ‖x‖ ^ 2

Tactic:
by
  refine and_congr_right fun _ ↦ forall₄_congr fun x _ y _ ↦ forall₅_congr fun a b ha hb hab ↦ ?_
  simp_rw [sub_le_iff_le_add, smul_eq_mul, aux_sub ha hb hab, mul_assoc, mul_left_comm]

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

Goal state before:
pp: V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed[inst✝²] s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z

Tactic:
let δ : ℝ := sInf t

Goal state after:
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed[inst✝²] s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z