mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
| ∑ a ∈ f.weights.support, f.weights a • ((Finset.affineCombination R a.weights.support id) ⇑a.weights -ᵥ b)

Tactic:
congr

Goal state after:
case s
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
| f.weights.support

case f
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
| fun a ↦ f.weights a • ((Finset.affineCombination R a.weights.support id) ⇑a.weights -ᵥ b)
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_9
M : Type u_10
I : Type u_11
J : Type u_12
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
f : StdSimplex R I
g : StdSimplex R J
e : I → J → M
⊢ iConvexComb (map (⇑(Equiv.prodComm I J)) (iConvexComb f fun i ↦ map (fun x ↦ (i, x)) g))
      (Function.uncurry e ∘ ⇑(Equiv.prodComm I J).symm) =
    iConvexComb (iConvexComb g fun i ↦ map (fun x ↦ (i, x)) f) (Function.uncurry fun j i ↦ e i j)

Tactic:
congr

Goal state after:
case e_s
R : Type u_9
M : Type u_10
I : Type u_11
J : Type u_12
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
f : StdSimplex R I
g : StdSimplex R J
e : I → J → M
⊢ map (⇑(Equiv.prodComm I J)) (iConvexComb f fun i ↦ map (fun x ↦ (i, x)) g) =
    iConvexComb g fun i ↦ map (fun x ↦ (i, x)) f
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
⊢ sConvexComb
      (StdSimplex.map f
        { weights := onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) ⋯, nonneg := ⋯, total := ⋯ }) =
    sConvexComb w

Tactic:
congr

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
⊢ StdSimplex.map f { weights := onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) ⋯, nonneg := ⋯, total := ⋯ } =
    w
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: 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
⊢ IsConvexSet K s

Tactic:
rintro w hw
  set t := w.weights.support with hsw
  have ht : t.Nonempty := w.support_weights_nonempty
  clear_value t
  induction ht using Finset.Nonempty.cons_induction generalizing w with
  | singleton x => simp_all [eq_comm]
  | cons x t hx ht ih =>
  have hwx : w.weights x ≠ 0 := by simpa using congr(x ∈ $hsw)
  have hwx' : ∃ y ≠ x, w.weights y ≠ 0 := by
    obtain ⟨y, hy⟩ := ht
    exact ⟨y, ne_of_mem_of_not_mem hy hx, by simpa [hy] using congr(y ∈ $hsw)⟩
  rw [← w.convexCombPair_restrict_restrict_compl {x} (by simpa) hwx']
  simp only [mem_singleton_iff, StdSimplex.restrict_singleton, sConvexComb_convexCombPair,
    sConvexComb_single]
  exact hs _ _ _ _ _ _ (hw <| by simp) _ <| ih (by grw [← hw, ← Finset.subset_cons])
    (by simp [← hsw]; grind)

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.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
x✝¹ : x ∈ Set.univ
y : E
x✝ : y ∈ Set.univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : a • x + b • y ≤ e
hc' : a • x + b • e ≤ a • x + b • y
⊢ a • f x + b • f e ≤ a • f x + b • g y

Tactic:
· rw [h_eq]
        gcongr
        exact h_mono Set.self_mem_Ici hy.le hy.le

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f : E → β
hf : QuasiconvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x < r}
⊢ StarConvex 𝕜 x {x | x ∈ s ∧ f x < r}

Tactic:
y

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f : E → β
hf : QuasiconvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x < r}
y : E
⊢ y ∈ {x | x ∈ s ∧ f x < r} → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ {x | x ∈ s ∧ f x < r}
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s✝ t✝ : ℝ
hs✝ : 0 ≤ s✝
ht✝ : 0 ≤ t✝
h✝ : s✝ + t✝ = 1
x✝ y : X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x : X
⊢ ∀ (y : X), dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y

Tactic:
y

Goal state after:
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s✝ t✝ : ℝ
hs✝ : 0 ≤ s✝
ht✝ : 0 ≤ t✝
h✝ : s✝ + t✝ = 1
x✝ y✝ : X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
⊢ dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x : X × X
⊢ ∀ (y : X × X),
    edist ((fun y ↦ convexCombPair (↑(i, y).1) (1 - ↑(i, y).1) ⋯ ⋯ ⋯ (i, y).2.1 (i, y).2.2) x)
        ((fun y ↦ convexCombPair (↑(i, y).1) (1 - ↑(i, y).1) ⋯ ⋯ ⋯ (i, y).2.1 (i, y).2.2) y) ≤
      ↑1 * edist x y

Tactic:
y

Goal state after:
case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ edist ((fun y ↦ convexCombPair (↑(i, y).1) (1 - ↑(i, y).1) ⋯ ⋯ ⋯ (i, y).2.1 (i, y).2.2) x)
      ((fun y ↦ convexCombPair (↑(i, y).1) (1 - ↑(i, y).1) ⋯ ⋯ ⋯ (i, y).2.1 (i, y).2.2) y) ≤
    ↑1 * edist x y
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ((convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t).Nonempty ∧
    ∀ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ≠ (convexHull 𝕜) ↑u
⊢ (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t = (convexHull 𝕜) ↑(s ∩ t)

Tactic:
· rw [coe_inter, convexHull_inter_convexHull hs ht]

Goal state after:
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
⊢ ↑i ∈ s.erase ↑j

Tactic:
simp [mem_erase, ne_of_mem_of_not_mem hi hj]

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

Goal state before:
pp: p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
⊢ StrictConcaveOn ℝ≥0 univ fun x ↦ x ^ p

Tactic:
let f := NNReal.orderIsoRpow (1 / p) hp₀'

Goal state after:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
⊢ StrictConcaveOn ℝ≥0 univ fun x ↦ x ^ p
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
⊢ fromEdgeSet ∅ = ⊥

Tactic:
by
  ext v w
  simp only [fromEdgeSet_adj, Set.mem_empty_iff_false, false_and, bot_adj]

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

Goal state before:
pp: case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
⊢ s.WOppSide x y → s.WOppSide y x

Tactic:
rintro ⟨p₁, hp₁, p₂, hp₂, h⟩

Goal state after:
case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder 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
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ s.WOppSide y x
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
s : Set (Set (Sym2 V))
⊢ fromEdgeSet (⋃₀ s) = sSup (fromEdgeSet '' s)

Tactic:
ext u v
  simp
  grind

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

Goal state before:
pp: case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
⊢ s.WOppSide y x → s.WOppSide x y

Tactic:
rintro ⟨p₁, hp₁, p₂, hp₂, h⟩

Goal state after:
case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder 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
h : SameRay R (y -ᵥ p₁) (p₂ -ᵥ x)
⊢ s.WOppSide x y
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.WSameSide (v +ᵥ x) y → s.WSameSide x y

Tactic:
rintro ⟨p₁, hp₁, p₂, hp₂, h⟩

Goal state after:
case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (y -ᵥ p₂)
⊢ s.WSameSide x y
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.WSameSide x y → s.WSameSide (v +ᵥ x) y

Tactic:
rintro ⟨p₁, hp₁, p₂, hp₂, h⟩

Goal state after:
case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ s.WSameSide (v +ᵥ x) y
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
v : V
e' : Sym2 V
he : e' ∈ G.edgeSet
h : v ∈ e'
⊢ (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'

Tactic:
exact ⟨⟨he, h⟩, he, Sym2.other_mem _⟩

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

Goal state before:
pp: case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.WOppSide (v +ᵥ x) y → s.WOppSide x y

Tactic:
rintro ⟨p₁, hp₁, p₂, hp₂, h⟩

Goal state after:
case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (p₂ -ᵥ y)
⊢ s.WOppSide x y
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.WOppSide x y → s.WOppSide (v +ᵥ x) y

Tactic:
rintro ⟨p₁, hp₁, p₂, hp₂, h⟩

Goal state after:
case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ s.WOppSide (v +ᵥ x) y
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✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t ≤ 0
⊢ SameRay R (-t • (p₁ -ᵥ x)) (p₁ -ᵥ x)

Tactic:
exact SameRay.sameRay_nonneg_smul_left _ (neg_nonneg.2 ht)

Goal state after:
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 = p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)

Tactic:
rw [vsub_left_cancel_iff] at h
    exact False.elim (hp₂p₃ h)

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

Goal state before:
pp: case mp
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 : P
⊢ s.WOppSide x x → x ∈ s

Tactic:
rintro ⟨p₁, hp₁, p₂, hp₂, h⟩

Goal state after:
case mp
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 p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
⊢ x ∈ s
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 : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : 0 ≤ 0
habz : bz = 1
⊢ v ∈ segment 𝕜 u v

Tactic:
by apply right_mem_segment

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * b * φ ‖x - y‖

Tactic:
rw [← sub_ne_zero, ← norm_pos_iff] at hxy

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : 0 < ‖x - y‖
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * b * φ ‖x - y‖
Module: Mathlib.Analysis.Convex.Strong

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * b * φ ‖x - y‖

Tactic:
rw [← sub_ne_zero, ← norm_pos_iff] at hxy

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : 0 < ‖x - y‖
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * b * φ ‖x - y‖
Module: Mathlib.Analysis.Convex.Visible

Goal state before:
pp: case inl
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝ : 0 < w i
hwi : w i = 1
⊢ IsVisible 𝕜 ((convexHull 𝕜) s) x (a i)

Tactic:
convert! hw

Goal state after:
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝ : 0 < w i
hwi : w i = 1
⊢ a i = ∑ i ∈ t, w i • a i
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
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
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
g_ae_nn : 0 ≤ᵐ[volume.restrict (Ioc 0 (f ω))] g
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ENNReal.ofReal (∫ (x : ℝ) in Ioc 0 (f ω), g x ∂volume)

Tactic:
congr

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
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
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
g_ae_nn : 0 ≤ᵐ[volume.restrict (Ioc 0 (f ω))] g
⊢ ∫ (t : ℝ) in 0..f ω, g t = ∫ (x : ℝ) in Ioc 0 (f ω), g x ∂volume
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
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
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : s ∉ Ioc 0 (f a)
h : 0 < s → f a < s
⊢ (Ioc 0 (f a)).indicator (fun t ↦ ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x ↦ 1) s * (Ici s).indicator (fun x ↦ 1) (f a)

Tactic:
by_cases h' : 0 < s

Goal state after:
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
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
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : s ∉ Ioc 0 (f a)
h : 0 < s → f a < s
h' : 0 < s
⊢ (Ioc 0 (f a)).indicator (fun t ↦ ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x ↦ 1) s * (Ici s).indicator (fun x ↦ 1) (f a)

case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
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
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : s ∉ Ioc 0 (f a)
h : 0 < s → f a < s
h' : ¬0 < s
⊢ (Ioc 0 (f a)).indicator (fun t ↦ ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x ↦ 1) s * (Ici s).indicator (fun x ↦ 1) (f a)
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✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w : Fin (n + 1) → R
hw : ∑ j, w j = 1
i : Fin (n + 1)
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).WSameSide
      ((Finset.affineCombination R Finset.univ s.points) (Pi.single i 1))
      ((Finset.affineCombination R Finset.univ s.points) w) ↔
    0 ≤ w i

Tactic:
s.wSameSide_affineSpan_faceOpposite_iff (Fintype.sum_pi_single' _ _) hw,

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✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w : Fin (n + 1) → R
hw : ∑ j, w j = 1
i : Fin (n + 1)
⊢ SignType.sign (Pi.single i 1 i) = SignType.sign (w i) ∨ Pi.single i 1 i = 0 ∨ w i = 0 ↔ 0 ≤ w i