-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
hx : x ∈ s ∪ t
inl :
  ∀ (h : x ∈ s),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inr :
  ∀ (h : x ∈ t),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inl₁ :
  ∀ (h : x ∈ s),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inr₁ :
  ∀ (h : x ∈ t),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inl₂ :
  ∀ (h : x ∈ s)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inr₂ :
  ∀ (h : x ∈ t)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inl₃ :
  ∀ (h : x ∈ s)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inr₃ :
  ∀ (h : x ∈ t)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inl₄ :
  ∀ (h : x ∈ s)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inr₄ :
  ∀ (h : x ∈ t)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inl₅ :
  ∀ (h : x ∈ s)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inr₅ :
  ∀ (h : x ∈ t)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inl₆ :
  ∀ (h : x ∈ s)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
    Subset (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F)
      ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F)
inr₆ :
  ∀ (h : x ∈ t)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)),
    Subset (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F)
      ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F)
inl₇ :
  ∀ (h : x ∈ s)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
    Subset (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F)
      ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F)
inr₇ :
  ∀ (h : x ∈ t)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)),
    Subset (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F)
      ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F)
inl₈ :
  ∀ (h : x ∈ s)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
    Subset (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F)
      ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F)
inr₈ :
  ∀ (h : x ∈ t)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)),
    Subset (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F)
      ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F)
inl₉ :
  ∀ (h : x ∈ s)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
    Subset (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F)
      ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F)
inr₉ :
  ∀ (h : x ∈ t)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)),
    Subset (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F)
      ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F)
inl₁₀ :
  ∀ (h : x ∈ s)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
    connectedComponentIn s x ⊆ connectedComponentIn (s ∪ t) x
inr₁₀ :
  ∀ (h : x ∈ t)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)),
    connectedComponentIn t x ⊆ connectedComponentIn (s ∪ t) x
inl₁₁ :
  ∀ (h : x ∈ s)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
    connectedComponentIn s x ⊆ connectedComponentIn (s ∪ t) x
inr₁₁ :
  ∀ (h : x ∈ t)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)),
    connectedComponentIn t x ⊆ connectedComponentIn (s ∪ t) x
inl₁₂ :
  ∀ (h : x ∈ s)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
    connectedComponentIn s x ⊆ connectedComponentIn (s ∪ t) x
inr₁₂ :
  ∀ (h : x ∈ t)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)),
    connectedComponentIn t x ⊆ connectedComponentIn (s ∪ t) x
inl₁₃ :
  ∀ (h : x ∈ s)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
    connectedComponentIn s x ⊆ connectedComponentIn (s ∪ t) x
inr₁₃ :
  ∀ (h : x ∈ t)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)),
    connectedComponentIn t x ⊆ connectedComponentIn (s ∪ t) x
inl₁₄ :
  ∀ (h : x ∈ s)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
    s ⊆ s ∪ t
inr₁₄ :
  ∀ (h : x ∈ t)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)),
    t ⊆ s ∪ t
inl₁₅ :
  ∀ (h : x ∈ s)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
    s ⊆ s ∪ t
inr₁₅ :
  ∀ (h : x ∈ t)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)),
    t ⊆ s ∪ t
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)

Tactic:
rcases hx with (h | h) <;>
  -- The connected component of `x ∈ s` in `s ∪ t` contains the connected component of `x` in `s`,
  -- hence is also full; similarly for `t`.
  [have hx := hs x h; have hx := ht x h] <;>
  rw [← Set.univ_subset_iff, ← hx] <;>
  apply convexHull_mono <;>
  apply connectedComponentIn_mono <;>
  [apply subset_union_left; apply subset_union_right]

Premises used: Set.univ_subset_iff, Set.subset_union_right, connectedComponentIn_mono, convexHull_mono, Set.subset_union_left