-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
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)
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
have 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)
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]
Cleared hypotheses: hx