awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
hx : x ∈ s
pos : IsConnected.{u_4} (α := P) {y : P | True}
⊢ IsConnected.{u_4} (α := P) {y : P | s.WSameSide x y}

Tactic:
simp only [wSameSide_of_left_mem, hx]

Premises used: AffineSubspace.wSameSide_of_left_mem
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
hx : x ∈ s
⊢ ConnectedSpace P

Tactic:
have := AddTorsor.connectedSpace V P
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ (↑s : Set P)
this_1 : Nonempty.{u_4 + 1} ↥s
hx : x ∈ s
this : ConnectedSpace P
⊢ IsConnected.{u_4} (α := P) {y : P | True}

Tactic:
isConnected_univ

Premises used: Set.univ, isConnected_univ
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ (↑s : Set P)
this_1 : Nonempty.{u_4 + 1} ↥s
hx : x ∈ s
this : ConnectedSpace P
⊢ IsConnected.{u_4} (α := P) {y : P | True}

Tactic:
exact isConnected_univ

Premises used: isConnected_univ
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
hx : x ∉ s
neg :
  IsConnected (α := P)
    ((fun (x_1 : ℝ × P) ↦ x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' SProd.sprod (α := Set ℝ) (Set.Ici 0) (↑s : Set P))
⊢ IsConnected.{u_4} (α := P) {y : P | s.WSameSide x y}

Tactic:
rw [setOf_wSameSide_eq_image2 hx hp, ← Set.image_prod]

Premises used: Set.image_prod, AffineSubspace.setOf_wSameSide_eq_image2
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
hx : x ∉ s
⊢ IsConnected (α := P)
    ((fun (x_1 : ℝ × P) ↦ x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' SProd.sprod (α := Set ℝ) (Set.Ici 0) (↑s : Set P))

Tactic:
(isConnected_Ici.prod (isConnected_iff_connectedSpace.2 ?_)).image _
      ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn

Premises used: Iff.mpr, Continuous.continuousOn, IsConnected.image, continuous_const, isConnected_Ici, continuous_snd, continuous_fst, Continuous.smul, Continuous.vadd, IsConnected.prod, isConnected_iff_connectedSpace
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
hx : x ∉ s
neg : ConnectedSpace.{u_4} (↑(↑s : Set P) : Type u_4)
⊢ IsConnected (α := P)
    ((fun (x_1 : ℝ × P) ↦ x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' SProd.sprod (α := Set ℝ) (Set.Ici 0) (↑s : Set P))

Tactic:
refine (isConnected_Ici.prod (isConnected_iff_connectedSpace.2 ?_)).image _
      ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn

Premises used: Iff.mpr, Continuous.continuousOn, IsConnected.image, continuous_const, isConnected_Ici, continuous_snd, continuous_fst, Continuous.smul, Continuous.vadd, IsConnected.prod, isConnected_iff_connectedSpace
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
hx : x ∉ s
⊢ ConnectedSpace.{u_4} ↥s

Tactic:
AddTorsor.connectedSpace s.direction s

Premises used: Membership.mem, Subtype, AddTorsor.connectedSpace, AffineSubspace.direction
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
hx : x ∉ s
⊢ ConnectedSpace.{u_4} (↑(↑s : Set P) : Type u_4)

Tactic:
convert! AddTorsor.connectedSpace s.direction s

Premises used: Membership.mem, Subtype, AddTorsor.connectedSpace, AffineSubspace.direction
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
inl : ∀ (h : (↑s : Set P) = ∅), IsPreconnected.{u_4} (α := P) {y : P | s.WSameSide x y}
inr : ∀ (h : (↑s : Set P).Nonempty), IsPreconnected.{u_4} (α := P) {y : P | s.WSameSide x y}
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.WSameSide x y}

Tactic:
rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)

Premises used: Set.eq_empty_or_nonempty, SetLike.coe
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s : Set P) = ∅
⊢ s = ⊥

Tactic:
rw [coe_eq_bot_iff] at h

Premises used: AffineSubspace.coe_eq_bot_iff
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
inl : IsPreconnected.{u_4} (α := P) {y : P | False}
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.WSameSide x y}

Tactic:
simp only [h, not_wSameSide_bot]

Premises used: AffineSubspace.not_wSameSide_bot
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
⊢ IsPreconnected.{u_4} (α := P) {y : P | False}

Tactic:
isPreconnected_empty

Premises used: setOf, isPreconnected_empty
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
⊢ IsPreconnected.{u_4} (α := P) {y : P | False}

Tactic:
exact isPreconnected_empty

Premises used: isPreconnected_empty
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s : Set P).Nonempty
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.WSameSide x y}

Tactic:
(isConnected_setOf_wSameSide x h).isPreconnected

Premises used: AffineSubspace.isConnected_setOf_wSameSide, IsConnected.isPreconnected
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s : Set P).Nonempty
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.WSameSide x y}

Tactic:
exact (isConnected_setOf_wSameSide x h).isPreconnected

Premises used: AffineSubspace.isConnected_setOf_wSameSide, IsConnected.isPreconnected
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
h : (↑s : Set P).Nonempty
obtain : ∀ (p : P) (hp : p ∈ (↑s : Set P)), IsConnected.{u_4} (α := P) {y : P | s.SSameSide x y}
⊢ IsConnected.{u_4} (α := P) {y : P | s.SSameSide x y}

Tactic:
obtain ⟨p, hp⟩ := h
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ (↑s : Set P)
⊢ Nonempty.{u_4 + 1} ↥s

Tactic:
haveI : Nonempty s := ⟨⟨p, hp⟩⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
rw :
  IsConnected (α := P)
    ((fun (x_1 : ℝ × P) ↦ x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' SProd.sprod (α := Set ℝ) (Set.Ioi 0) (↑s : Set P))
⊢ IsConnected.{u_4} (α := P) {y : P | s.SSameSide x y}

Tactic:
rw [setOf_sSameSide_eq_image2 hx hp, ← Set.image_prod]

Premises used: AffineSubspace.setOf_sSameSide_eq_image2, Set.image_prod
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
⊢ IsConnected (α := P)
    ((fun (x_1 : ℝ × P) ↦ x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' SProd.sprod (α := Set ℝ) (Set.Ioi 0) (↑s : Set P))

Tactic:
(isConnected_Ioi.prod (isConnected_iff_connectedSpace.2 ?_)).image _
    ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn

Premises used: Iff.mpr, Continuous.continuousOn, IsConnected.image, continuous_const, continuous_snd, continuous_fst, Continuous.smul, Continuous.vadd, IsConnected.prod, isConnected_Ioi, isConnected_iff_connectedSpace
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
refine : ConnectedSpace.{u_4} (↑(↑s : Set P) : Type u_4)
⊢ IsConnected (α := P)
    ((fun (x_1 : ℝ × P) ↦ x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' SProd.sprod (α := Set ℝ) (Set.Ioi 0) (↑s : Set P))

Tactic:
refine (isConnected_Ioi.prod (isConnected_iff_connectedSpace.2 ?_)).image _
    ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn

Premises used: Iff.mpr, Continuous.continuousOn, IsConnected.image, continuous_const, continuous_snd, continuous_fst, Continuous.smul, Continuous.vadd, IsConnected.prod, isConnected_Ioi, isConnected_iff_connectedSpace
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
⊢ ConnectedSpace.{u_4} ↥s

Tactic:
AddTorsor.connectedSpace s.direction s

Premises used: Membership.mem, Subtype, AddTorsor.connectedSpace, AffineSubspace.direction
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
⊢ ConnectedSpace.{u_4} (↑(↑s : Set P) : Type u_4)

Tactic:
convert! AddTorsor.connectedSpace s.direction s

Premises used: Membership.mem, Subtype, AddTorsor.connectedSpace, AffineSubspace.direction
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
inl : ∀ (h : (↑s : Set P) = ∅), IsPreconnected.{u_4} (α := P) {y : P | s.SSameSide x y}
inr : ∀ (h : (↑s : Set P).Nonempty), IsPreconnected.{u_4} (α := P) {y : P | s.SSameSide x y}
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SSameSide x y}

Tactic:
rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)

Premises used: Set.eq_empty_or_nonempty, SetLike.coe
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
inl : IsPreconnected.{u_4} (α := P) {y : P | False}
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SSameSide x y}

Tactic:
simp only [h, not_sSameSide_bot]

Premises used: AffineSubspace.not_sSameSide_bot
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s : Set P).Nonempty
pos : ∀ (hx : x ∈ s), IsPreconnected.{u_4} (α := P) {y : P | s.SSameSide x y}
neg : ∀ (hx : x ∉ s), IsPreconnected.{u_4} (α := P) {y : P | s.SSameSide x y}
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SSameSide x y}

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s : Set P).Nonempty
hx : x ∈ s
pos : IsPreconnected.{u_4} (α := P) {y : P | False}
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SSameSide x y}

Tactic:
simp only [hx, SSameSide, not_true, false_and, and_false]

Premises used: AffineSubspace.SSameSide, false_and, not_true, and_false
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s : Set P).Nonempty
hx : x ∈ s
⊢ IsPreconnected.{u_4} (α := P) {y : P | False}

Tactic:
isPreconnected_empty

Premises used: setOf, isPreconnected_empty
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s : Set P).Nonempty
hx : x ∈ s
⊢ IsPreconnected.{u_4} (α := P) {y : P | False}

Tactic:
exact isPreconnected_empty

Premises used: isPreconnected_empty
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s : Set P).Nonempty
hx : x ∉ s
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SSameSide x y}

Tactic:
(isConnected_setOf_sSameSide hx h).isPreconnected

Premises used: IsConnected.isPreconnected, AffineSubspace.isConnected_setOf_sSameSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s : Set P).Nonempty
hx : x ∉ s
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SSameSide x y}

Tactic:
exact (isConnected_setOf_sSameSide hx h).isPreconnected

Premises used: IsConnected.isPreconnected, AffineSubspace.isConnected_setOf_sSameSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s : Set P).Nonempty
obtain : ∀ (p : P) (hp : p ∈ (↑s : Set P)), IsConnected.{u_4} (α := P) {y : P | s.WOppSide x y}
⊢ IsConnected.{u_4} (α := P) {y : P | s.WOppSide x y}

Tactic:
obtain ⟨p, hp⟩ := h
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
pos : ∀ (hx : x ∈ s), IsConnected.{u_4} (α := P) {y : P | s.WOppSide x y}
neg : ∀ (hx : x ∉ s), IsConnected.{u_4} (α := P) {y : P | s.WOppSide x y}
⊢ IsConnected.{u_4} (α := P) {y : P | s.WOppSide x y}

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
hx : x ∈ s
pos : IsConnected.{u_4} (α := P) {y : P | True}
⊢ IsConnected.{u_4} (α := P) {y : P | s.WOppSide x y}

Tactic:
simp only [wOppSide_of_left_mem, hx]

Premises used: AffineSubspace.wOppSide_of_left_mem
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
hx : x ∉ s
neg :
  IsConnected (α := P)
    ((fun (x_1 : ℝ × P) ↦ x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' SProd.sprod (α := Set ℝ) (Set.Iic 0) (↑s : Set P))
⊢ IsConnected.{u_4} (α := P) {y : P | s.WOppSide x y}

Tactic:
rw [setOf_wOppSide_eq_image2 hx hp, ← Set.image_prod]

Premises used: Set.image_prod, AffineSubspace.setOf_wOppSide_eq_image2
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
hx : x ∉ s
⊢ IsConnected (α := P)
    ((fun (x_1 : ℝ × P) ↦ x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' SProd.sprod (α := Set ℝ) (Set.Iic 0) (↑s : Set P))

Tactic:
(isConnected_Iic.prod (isConnected_iff_connectedSpace.2 ?_)).image _
      ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn

Premises used: Iff.mpr, Continuous.continuousOn, IsConnected.image, continuous_const, continuous_snd, continuous_fst, Continuous.smul, Continuous.vadd, isConnected_Iic, IsConnected.prod, isConnected_iff_connectedSpace
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
hx : x ∉ s
neg : ConnectedSpace.{u_4} (↑(↑s : Set P) : Type u_4)
⊢ IsConnected (α := P)
    ((fun (x_1 : ℝ × P) ↦ x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' SProd.sprod (α := Set ℝ) (Set.Iic 0) (↑s : Set P))

Tactic:
refine (isConnected_Iic.prod (isConnected_iff_connectedSpace.2 ?_)).image _
      ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn

Premises used: Iff.mpr, Continuous.continuousOn, IsConnected.image, continuous_const, continuous_snd, continuous_fst, Continuous.smul, Continuous.vadd, isConnected_Iic, IsConnected.prod, isConnected_iff_connectedSpace
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
inl : ∀ (h : (↑s : Set P) = ∅), IsPreconnected.{u_4} (α := P) {y : P | s.WOppSide x y}
inr : ∀ (h : (↑s : Set P).Nonempty), IsPreconnected.{u_4} (α := P) {y : P | s.WOppSide x y}
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.WOppSide x y}

Tactic:
rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)

Premises used: Set.eq_empty_or_nonempty, SetLike.coe
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
inl : IsPreconnected.{u_4} (α := P) {y : P | False}
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.WOppSide x y}

Tactic:
simp only [h, not_wOppSide_bot]

Premises used: AffineSubspace.not_wOppSide_bot
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s : Set P).Nonempty
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.WOppSide x y}

Tactic:
(isConnected_setOf_wOppSide x h).isPreconnected

Premises used: AffineSubspace.isConnected_setOf_wOppSide, IsConnected.isPreconnected
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s : Set P).Nonempty
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.WOppSide x y}

Tactic:
exact (isConnected_setOf_wOppSide x h).isPreconnected

Premises used: AffineSubspace.isConnected_setOf_wOppSide, IsConnected.isPreconnected
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
h : (↑s : Set P).Nonempty
obtain : ∀ (p : P) (hp : p ∈ (↑s : Set P)), IsConnected.{u_4} (α := P) {y : P | s.SOppSide x y}
⊢ IsConnected.{u_4} (α := P) {y : P | s.SOppSide x y}

Tactic:
obtain ⟨p, hp⟩ := h
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
rw :
  IsConnected (α := P)
    ((fun (x_1 : ℝ × P) ↦ x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' SProd.sprod (α := Set ℝ) (Set.Iio 0) (↑s : Set P))
⊢ IsConnected.{u_4} (α := P) {y : P | s.SOppSide x y}

Tactic:
rw [setOf_sOppSide_eq_image2 hx hp, ← Set.image_prod]

Premises used: Set.image_prod, AffineSubspace.setOf_sOppSide_eq_image2
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
⊢ IsConnected (α := P)
    ((fun (x_1 : ℝ × P) ↦ x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' SProd.sprod (α := Set ℝ) (Set.Iio 0) (↑s : Set P))

Tactic:
(isConnected_Iio.prod (isConnected_iff_connectedSpace.2 ?_)).image _
    ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn

Premises used: Iff.mpr, Continuous.continuousOn, IsConnected.image, isConnected_Iio, continuous_const, continuous_snd, continuous_fst, Continuous.smul, Continuous.vadd, IsConnected.prod, isConnected_iff_connectedSpace
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ (↑s : Set P)
this : Nonempty.{u_4 + 1} ↥s
refine : ConnectedSpace.{u_4} (↑(↑s : Set P) : Type u_4)
⊢ IsConnected (α := P)
    ((fun (x_1 : ℝ × P) ↦ x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' SProd.sprod (α := Set ℝ) (Set.Iio 0) (↑s : Set P))

Tactic:
refine (isConnected_Iio.prod (isConnected_iff_connectedSpace.2 ?_)).image _
    ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn

Premises used: Iff.mpr, Continuous.continuousOn, IsConnected.image, isConnected_Iio, continuous_const, continuous_snd, continuous_fst, Continuous.smul, Continuous.vadd, IsConnected.prod, isConnected_iff_connectedSpace
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
inl : ∀ (h : (↑s : Set P) = ∅), IsPreconnected.{u_4} (α := P) {y : P | s.SOppSide x y}
inr : ∀ (h : (↑s : Set P).Nonempty), IsPreconnected.{u_4} (α := P) {y : P | s.SOppSide x y}
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SOppSide x y}

Tactic:
rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)

Premises used: Set.eq_empty_or_nonempty, SetLike.coe