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

Goal state before:
pp: I : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst✝¹ : Zero X
inst✝ : ConvexSpace R X
i : ι
w : StdSimplex R (StdSimplex R (ι →₀ X))
⊢ onFinset
      ((StdSimplex.map (fun w ↦ onFinset (w.weights.support.biUnion support) (fun i ↦ iConvexComb w fun x ↦ x i) ⋯)
                w).weights.support.biUnion
        support)
      (fun i ↦
        iConvexComb
          (StdSimplex.map (fun w ↦ onFinset (w.weights.support.biUnion support) (fun i ↦ iConvexComb w fun x ↦ x i) ⋯)
            w)
          fun x ↦ x i)
      ⋯ =
    onFinset ((sConvexComb w).weights.support.biUnion support) (fun i ↦ iConvexComb (sConvexComb w) fun x ↦ x i) ⋯

Tactic:
ext

Goal state after:
I : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst✝¹ : Zero X
inst✝ : ConvexSpace R X
i : ι
w : StdSimplex R (StdSimplex R (ι →₀ X))
a✝ : ι
⊢ (onFinset
        ((StdSimplex.map (fun w ↦ onFinset (w.weights.support.biUnion support) (fun i ↦ iConvexComb w fun x ↦ x i) ⋯)
                  w).weights.support.biUnion
          support)
        (fun i ↦
          iConvexComb
            (StdSimplex.map (fun w ↦ onFinset (w.weights.support.biUnion support) (fun i ↦ iConvexComb w fun x ↦ x i) ⋯)
              w)
            fun x ↦ x i)
        ⋯)
      a✝ =
    (onFinset ((sConvexComb w).weights.support.biUnion support) (fun i ↦ iConvexComb (sConvexComb w) fun x ↦ x i) ⋯) a✝
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
w : StdSimplex R I
f g : I → M
hfg : ∀ (i : I), w.weights i ≠ 0 → f i = g i
⊢ iConvexComb w f = iConvexComb w g

Tactic:
by
  refine congr(sConvexComb $(?_))
  ext i
  simp only [weights_map]
  -- TODO: This should just be `congr! 2 with i hi`.
  congr 1
  refine Finsupp.mapDomain_congr fun i hi ↦ ?_
  exact hfg i (by simpa using hi)

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

Goal state before:
pp: ι : Type u_1
I : Type u_2
R : Type u_3
K : Type u_4
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
w✝ : StdSimplex R X
s✝ t : Set X
x y : X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R (StdSimplex R ↑s)
⊢ ⟨iConvexComb (StdSimplex.map (fun w ↦ ⟨iConvexComb w Subtype.val, ⋯⟩) w) Subtype.val, ⋯⟩ =
    ⟨iConvexComb (sConvexComb w) Subtype.val, ⋯⟩

Tactic:
ext

Goal state after:
ι : Type u_1
I : Type u_2
R : Type u_3
K : Type u_4
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
w✝ : StdSimplex R X
s✝ t : Set X
x y : X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R (StdSimplex R ↑s)
⊢ ↑⟨iConvexComb (StdSimplex.map (fun w ↦ ⟨iConvexComb w Subtype.val, ⋯⟩) w) Subtype.val, ⋯⟩ =
    ↑⟨iConvexComb (sConvexComb w) Subtype.val, ⋯⟩
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: case refine_2
R : Type u_3
X : Type u_5
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
s : Set X
Y : Type u_7
inst✝ : ConvexSpace R Y
t : Set Y
hs : IsConvexSet R s
ht : IsConvexSet R t
w : StdSimplex R (X × Y)
hw : ↑w.weights.support ⊆ s ×ˢ t
⊢ ↑(StdSimplex.map Prod.snd w).weights.support ⊆ t

Tactic:
grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, snd_image_prod_subset]

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
⊢ ConvexOn 𝕜 Set.univ ((Set.Iic e).piecewise f g)

Tactic:
refine ⟨convex_univ, fun x _ y _ a b ha hb hab ↦ ?_⟩
  obtain hx | hx := le_or_gt x e <;> obtain hy | hy := le_or_gt y e
  · have hc : a • x + b • y ≤ e := (Convex.combo_le_max x y ha hb hab).trans (max_le hx hy)
    rw [Set.piecewise_eq_of_mem (Set.Iic e) f g hx, Set.piecewise_eq_of_mem (Set.Iic e) f g hy,
      Set.piecewise_eq_of_mem (Set.Iic e) f g hc]
    exact hf.2 hx hy ha hb hab
  · rw [Set.piecewise_eq_of_mem (Set.Iic e) f g hx,
      Set.piecewise_eq_of_notMem (Set.Iic e) f g (Set.notMem_Iic.mpr hy)]
    obtain hc | hc := le_or_gt (a • x + b • y) e
    · rw [Set.piecewise_eq_of_mem (Set.Iic e) f g hc]
      have hc' : a • x + b • e ≤ a • x + b • y := by gcongr
      trans a • f x + b • f e
      · exact (h_anti (hc'.trans hc) hc hc').trans (hf.2 hx Set.self_mem_Iic ha hb hab)
      · rw [h_eq]
        gcongr
        exact h_mono Set.self_mem_Ici hy.le hy.le
    · rw [Set.piecewise_eq_of_notMem (Set.Iic e) f g (Set.notMem_Iic.mpr hc)]
      have hc' : a • x + b • y ≤ a • e + b • y := by gcongr
      trans a • g e + b • g y
      · exact (h_mono hc.le (hc.le.trans hc') hc').trans (hg.2 Set.self_mem_Ici hy.le ha hb hab)
      · rw [← h_eq]
        gcongr
        exact h_anti hx Set.self_mem_Iic hx
  · rw [Set.piecewise_eq_of_notMem (Set.Iic e) f g (Set.notMem_Iic.mpr hx),
      Set.piecewise_eq_of_mem (Set.Iic e) f g hy]
    obtain hc | hc := le_or_gt (a • x + b • y) e
    · rw [Set.piecewise_eq_of_mem (Set.Iic e) f g hc]
      have hc' : a • e + b • y ≤ a • x + b • y := by gcongr
      trans a • f e + b • f y
      · exact (h_anti (hc'.trans hc) hc hc').trans (hf.2 Set.self_mem_Iic hy ha hb hab)
      · rw [h_eq]
        gcongr
        exact h_mono Set.self_mem_Ici hx.le hx.le
    · rw [Set.piecewise_eq_of_notMem (Set.Iic e) f g (Set.notMem_Iic.mpr hc)]
      have hc' : a • x + b • y ≤ a • x + b • e := by gcongr
      trans a • g x + b • g e
      · exact (h_mono hc.le (hc.le.trans hc') hc').trans (hg.2 hx.le Set.self_mem_Ici ha hb hab)
      · rw [← h_eq]
        gcongr
        exact h_anti hy Set.self_mem_Iic hy
  · have hc : e < a • x + b • y :=
        (lt_min hx hy).trans_le (Convex.min_le_combo x y ha hb hab)
    rw [(Set.Iic e).piecewise_eq_of_notMem f g (Set.notMem_Iic.mpr hx),
      (Set.Iic e).piecewise_eq_of_notMem f g (Set.notMem_Iic.mpr hy),
      (Set.Iic e).piecewise_eq_of_notMem f g (Set.notMem_Iic.mpr hc)]
    exact hg.2 hx.le hy.le ha hb hab

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

Goal state before:
pp: F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst✝¹³ : Semiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsStrictOrderedRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : SetLike F M
inst✝⁵ : AddSubmonoidClass F M
inst✝⁴ : SMulMemClass F R M
f g : M → N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
x y : M
s t : Set M
a b : R
S : F
w : StdSimplex R ↥S
⊢ sConvexComb w = w.weights.sum fun m r ↦ r • m

Tactic:
ext

Goal state after:
F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst✝¹³ : Semiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsStrictOrderedRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : SetLike F M
inst✝⁵ : AddSubmonoidClass F M
inst✝⁴ : SMulMemClass F R M
f g : M → N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
x y : M
s t : Set M
a b : R
S : F
w : StdSimplex R ↥S
⊢ ↑(sConvexComb w) = ↑(w.weights.sum fun m r ↦ r • m)
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst✝¹³ : Semiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsStrictOrderedRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : SetLike F M
inst✝⁵ : AddSubmonoidClass F M
inst✝⁴ : SMulMemClass F R M
f g : M → N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
x y : M
s t : Set M
a b : R
w : StdSimplex R (M × N)
⊢ sConvexComb w = w.weights.sum fun m r ↦ r • m

Tactic:
ext

Goal state after:
case fst
F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst✝¹³ : Semiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsStrictOrderedRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : SetLike F M
inst✝⁵ : AddSubmonoidClass F M
inst✝⁴ : SMulMemClass F R M
f g : M → N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
x y : M
s t : Set M
a b : R
w : StdSimplex R (M × N)
⊢ (sConvexComb w).1 = (w.weights.sum fun m r ↦ r • m).1

case snd
F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst✝¹³ : Semiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsStrictOrderedRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : SetLike F M
inst✝⁵ : AddSubmonoidClass F M
inst✝⁴ : SMulMemClass F R M
f g : M → N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
x y : M
s t : Set M
a b : R
w : StdSimplex R (M × N)
⊢ (sConvexComb w).2 = (w.weights.sum fun m r ↦ r • m).2
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: F : Type u_1
R : Type u_2
M✝ : Type u_3
N : Type u_4
I : Type u_5
inst✝¹⁷ : Semiring R
inst✝¹⁶ : PartialOrder R
inst✝¹⁵ : IsStrictOrderedRing R
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : Module R M✝
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : SetLike F M✝
inst✝⁹ : AddSubmonoidClass F M✝
inst✝⁸ : SMulMemClass F R M✝
f g : M✝ → N
inst✝⁷ : ConvexSpace R M✝
inst✝⁶ : IsModuleConvexSpace R M✝
inst✝⁵ : ConvexSpace R N
inst✝⁴ : IsModuleConvexSpace R N
x y : M✝
s t : Set M✝
a b : R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → ConvexSpace R (M i)
inst✝ : ∀ (i : ι), IsModuleConvexSpace R (M i)
w : StdSimplex R ((i : ι) → M i)
⊢ sConvexComb w = w.weights.sum fun m r ↦ r • m

Tactic:
ext

Goal state after:
F : Type u_1
R : Type u_2
M✝ : Type u_3
N : Type u_4
I : Type u_5
inst✝¹⁷ : Semiring R
inst✝¹⁶ : PartialOrder R
inst✝¹⁵ : IsStrictOrderedRing R
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : Module R M✝
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : SetLike F M✝
inst✝⁹ : AddSubmonoidClass F M✝
inst✝⁸ : SMulMemClass F R M✝
f g : M✝ → N
inst✝⁷ : ConvexSpace R M✝
inst✝⁶ : IsModuleConvexSpace R M✝
inst✝⁵ : ConvexSpace R N
inst✝⁴ : IsModuleConvexSpace R N
x y : M✝
s t : Set M✝
a b : R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → ConvexSpace R (M i)
inst✝ : ∀ (i : ι), IsModuleConvexSpace R (M i)
w : StdSimplex R ((i : ι) → M i)
x✝ : ι
⊢ sConvexComb w x✝ = w.weights.sum (fun m r ↦ r • m) x✝
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst✝¹³ : Semiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsStrictOrderedRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : SetLike F M
inst✝⁵ : AddSubmonoidClass F M
inst✝⁴ : SMulMemClass F R M
f g : M → N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
x y : M
s t : Set M
a b : R
ι : Type u_6
w : StdSimplex R (ι →₀ M)
⊢ sConvexComb w = w.weights.sum fun m r ↦ r • m

Tactic:
ext

Goal state after:
F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst✝¹³ : Semiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsStrictOrderedRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : SetLike F M
inst✝⁵ : AddSubmonoidClass F M
inst✝⁴ : SMulMemClass F R M
f g : M → N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
x y : M
s t : Set M
a b : R
ι : Type u_6
w : StdSimplex R (ι →₀ M)
a✝ : ι
⊢ (sConvexComb w) a✝ = (w.weights.sum fun m r ↦ r • m) a✝
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
⊢ (⋂ i ∈ s, F i).Nonempty

Tactic:
let a (i : s) : E := Set.Nonempty.some (s := ⋂ j ∈ s.erase i, F j) <| by
    apply hk (s := s.erase i)
    · exact fun i hi ↦ h_convex i (mem_of_mem_erase hi)
    · intro J hJ_ss hJ_card
      exact h_inter J (subset_trans hJ_ss (erase_subset i.val s)) hJ_card
    · simp only [coe_mem, card_erase_of_mem]; lia
  /- This family of vectors is not affine independent because the number of them exceeds the
  dimension of the space. -/
  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
  /- Use `radon_partition` to conclude there is a subset `I` of `s` and a point `p : E` which
  lies in the convex hull of either `a '' I` or `a '' Iᶜ`. We claim that `p ∈ ⋂ i ∈ s, F i`. -/
  obtain ⟨I, p, hp_I, hp_Ic⟩ := radon_partition h_ind
  use p
  apply mem_biInter
  intro i hi
  lift i to s using hi
  /- It suffices to show that for any subcollection `J` of `s` containing `i`, the convex
  hull of `a '' (s \ J)` is contained in `F i`. -/
  suffices ∀ J : Set s, (i ∈ J) → (convexHull 𝕜) (a '' Jᶜ) ⊆ F i by
    by_cases h : i ∈ I
    · exact this I h hp_Ic
    · apply this Iᶜ h; rwa [compl_compl]
  /- Given any subcollection `J` of `ι` containing `i`, because `F i` is convex, we need only
  show that `a j ∈ F i` for each `j ∈ s \ J`. -/
  intro J hi
  rw [convexHull_subset_iff (h_convex i.1 i.2)]
  rintro v ⟨j, hj, hj_v⟩
  rw [← hj_v]
  /- Since `j ∈ Jᶜ` and `i ∈ J`, we conclude that `i ≠ j`, and hence by the definition of `a`:
  `a j ∈ ⋂ F '' (Set.univ \ {j}) ⊆ F i`. -/
  apply mem_of_subset_of_mem (s₁ := ⋂ k ∈ (s.erase j), F k)
  · apply iInter₂_subset
    simp [mem_erase, ne_of_mem_of_not_mem hi hj]
  · apply Nonempty.some_mem

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
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ ⋂₀ ↑F = ⋂ X ∈ F, X

Tactic:
ext

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
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
x✝ : E
⊢ x✝ ∈ ⋂₀ ↑F ↔ x✝ ∈ ⋂ X ∈ F, X
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
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
⊢ ⋂ X ∈ G, X = ⋂₀ ↑G

Tactic:
ext

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
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
x✝ : E
⊢ x✝ ∈ ⋂ X ∈ G, X ↔ x✝ ∈ ⋂₀ ↑G
Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : DecidableEq ι
G : SimpleGraph ι
e : Sym2 ι
he : e ∈ G.edgeSet
⊢ e.toFinset.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ⊆ e.toFinset → b.Nonempty → b ∈ {s | ∃ v, s = {v}} ∪ Sym2.toFinset '' G.edgeSet

Tactic:
constructor

Goal state after:
case inr.left
ι : Type u_1
inst✝ : DecidableEq ι
G : SimpleGraph ι
e : Sym2 ι
he : e ∈ G.edgeSet
⊢ e.toFinset.Nonempty

case inr.right
ι : Type u_1
inst✝ : DecidableEq ι
G : SimpleGraph ι
e : Sym2 ι
he : e ∈ G.edgeSet
⊢ ∀ ⦃b : Finset ι⦄, b ⊆ e.toFinset → b.Nonempty → b ∈ {s | ∃ v, s = {v}} ∪ Sym2.toFinset '' G.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case refine_3
V : Type u
inst✝¹ : Fintype V
inst✝ : DecidableEq V
Adj : V → V → Prop
hs : Std.Symm Adj
hi : Std.Irrefl Adj
⊢ SimpleGraph.mk' ⟨fun v w ↦ decide (Adj v w), ⋯⟩ = { Adj := Adj, symm := hs, loopless := hi }

Tactic:
ext

Goal state after:
case refine_3
V : Type u
inst✝¹ : Fintype V
inst✝ : DecidableEq V
Adj : V → V → Prop
hs : Std.Symm Adj
hi : Std.Irrefl Adj
x✝¹ x✝ : V
⊢ (SimpleGraph.mk' ⟨fun v w ↦ decide (Adj v w), ⋯⟩).Adj x✝¹ x✝ ↔ { Adj := Adj, symm := hs, loopless := hi }.Adj x✝¹ x✝
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
ι✝ : Type u
κ✝ : ι✝ → Type u
f : (a : ι✝) → κ✝ a → SimpleGraph V
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
ext

Goal state after:
ι : Sort u_1
V : Type u
G H : SimpleGraph V
a b c u v w : V
e : Sym2 V
ι✝ : Type u
κ✝ : ι✝ → Type u
f : (a : ι✝) → κ✝ a → SimpleGraph V
x✝¹ x✝ : V
⊢ (⨅ a, ⨆ b, f a b).Adj x✝¹ x✝ ↔ (⨆ g, ⨅ a, f a (g a)).Adj x✝¹ x✝
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_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
⊢ ⋂₀ F = ⋂ X, ↑X

Tactic:
ext

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_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
x✝ : E
⊢ x✝ ∈ ⋂₀ F ↔ x✝ ∈ ⋂ X, ↑X
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
ι : Sort u_2
inst✝ : Nonempty ι
f : ι → SimpleGraph V
⊢ (⨅ i, f i).edgeSet = ⋂ i, (f i).edgeSet

Tactic:
ext ⟨x, y⟩
  have ⟨i⟩ := ‹Nonempty ι›
  simpa using (· i |>.ne)

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
⊢ (↑I).encard ≤ ↑(finrank 𝕜 E) + 1

Tactic:
by norm_cast

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

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsStrictOrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective ⇑f
⊢ (map f s).WSameSide (f x) (f y) ↔ s.WSameSide x y

Tactic:
refine ⟨fun h => ?_, fun h => h.map _⟩
  rcases h with ⟨fp₁, hfp₁, fp₂, hfp₂, h⟩
  rw [mem_map] at hfp₁ hfp₂
  rcases hfp₁ with ⟨p₁, hp₁, rfl⟩
  rcases hfp₂ with ⟨p₂, hp₂, rfl⟩
  refine ⟨p₁, hp₁, p₂, hp₂, ?_⟩
  simp_rw [← linearMap_vsub, (f.linear_injective_iff.2 hf).sameRay_map_iff] at h
  exact h

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

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsStrictOrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective ⇑f
⊢ (map f s).WOppSide (f x) (f y) ↔ s.WOppSide x y

Tactic:
refine ⟨fun h => ?_, fun h => h.map _⟩
  rcases h with ⟨fp₁, hfp₁, fp₂, hfp₂, h⟩
  rw [mem_map] at hfp₁ hfp₂
  rcases hfp₁ with ⟨p₁, hp₁, rfl⟩
  rcases hfp₂ with ⟨p₂, hp₂, rfl⟩
  refine ⟨p₁, hp₁, p₂, hp₂, ?_⟩
  simp_rw [← linearMap_vsub, (f.linear_injective_iff.2 hf).sameRay_map_iff] at h
  exact h

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

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsStrictOrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective ⇑f
⊢ (map f s).SOppSide (f x) (f y) ↔ s.SOppSide x y

Tactic:
simp_rw [SOppSide, hf.wOppSide_map_iff, mem_map_iff_mem_of_injective hf]

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

Goal state before:
pp: p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := NNReal.mk x hx
y' : ℝ≥0 := NNReal.mk y hy
a' : ℝ≥0 := NNReal.mk a ⋯
b' : ℝ≥0 := NNReal.mk b ⋯
hxy' : x' ≠ y'
⊢ a' + b' = 1

Tactic:
ext

Goal state after:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := ⋯
y' : ℝ≥0 := ⋯
a' : ℝ≥0 := ⋯
b' : ℝ≥0 := ⋯
hxy' : x' ≠ y'
⊢ ↑(a' + b') = ↑1
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
⊢ fromEdgeSet Sym2.diagSetᶜ = ⊤

Tactic:
ext

Goal state after:
V : Type u
x✝¹ x✝ : V
⊢ (fromEdgeSet Sym2.diagSetᶜ).Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : 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:
constructor

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
⊢ s.WOppSide x y → s.WOppSide y x

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