awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ IsConnected.{u_4} (α := P) {y : P | s.WSameSide x y}
have pos : ∀ (hx : x ∈ s), IsConnected.{u_4} (α := P) {y : P | s.WSameSide x y}
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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.WSameSide x y}
⊢ IsConnected.{u_4} (α := P) {y : P | s.WSameSide x y}
have neg : ∀ (hx : x ∉ s), IsConnected.{u_4} (α := P) {y : P | s.WSameSide x y}
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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.{u_4} (α := P) {y : P | s.WSameSide x y}
have pos : IsConnected.{u_4} (α := P) {y : P | True}
Tactic: simp only [wSameSide_of_left_mem, hx]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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.{u_4} (α := P) {y : P | True}
have this₁ : ConnectedSpace P
Tactic: have := AddTorsor.connectedSpace V P
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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.{u_4} (α := P) {y : P | s.WSameSide x y}
have neg : IsConnected (α := P)
  ((fun (x_1 : ℝ × P) ↦ x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' SProd.sprod (α := Set ℝ) (Set.Ici 0) (↑s : Set P))
Tactic: rw [setOf_wSameSide_eq_image2 hx hp, ← Set.image_prod]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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))
have neg : ConnectedSpace.{u_4} (↑(↑s : Set P) : Type u_4)
Tactic: refine (isConnected_Ici.prod (isConnected_iff_connectedSpace.2 ?_)).image _
      ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.WSameSide x y}
have inl : ∀ (h : (↑s : Set P) = ∅), IsPreconnected.{u_4} (α := P) {y : P | s.WSameSide x y}
Tactic: rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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}
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.WSameSide x y}
have inr : ∀ (h : (↑s : Set P).Nonempty), IsPreconnected.{u_4} (α := P) {y : P | s.WSameSide x y}
Tactic: rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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) = ∅
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.WSameSide x y}
have h₁ : s = ⊥
Tactic: rw [coe_eq_bot_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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 | s.WSameSide x y}
have inl : IsPreconnected.{u_4} (α := P) {y : P | False}
Tactic: simp only [h, not_wSameSide_bot]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ IsConnected.{u_4} (α := P) {y : P | s.SSameSide x y}
have obtain : ∀ (p : P) (hp : p ∈ (↑s : Set P)), IsConnected.{u_4} (α := P) {y : P | s.SSameSide x y}
Tactic: obtain ⟨p, hp⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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)
⊢ IsConnected.{u_4} (α := P) {y : P | s.SSameSide x y}
have this : Nonempty.{u_4 + 1} ↥s
Tactic: haveI : Nonempty s := ⟨⟨p, hp⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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.{u_4} (α := P) {y : P | s.SSameSide x y}
have rw : IsConnected (α := P)
  ((fun (x_1 : ℝ × P) ↦ x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' SProd.sprod (α := Set ℝ) (Set.Ioi 0) (↑s : Set P))
Tactic: rw [setOf_sSameSide_eq_image2 hx hp, ← Set.image_prod]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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))
have refine : ConnectedSpace.{u_4} (↑(↑s : Set P) : Type u_4)
Tactic: refine (isConnected_Ioi.prod (isConnected_iff_connectedSpace.2 ?_)).image _
    ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SSameSide x y}
have inl : ∀ (h : (↑s : Set P) = ∅), IsPreconnected.{u_4} (α := P) {y : P | s.SSameSide x y}
Tactic: rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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}
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SSameSide x y}
have inr : ∀ (h : (↑s : Set P).Nonempty), IsPreconnected.{u_4} (α := P) {y : P | s.SSameSide x y}
Tactic: rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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) = ∅
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SSameSide x y}
have h₁ : s = ⊥
Tactic: rw [coe_eq_bot_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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 | s.SSameSide x y}
have inl : IsPreconnected.{u_4} (α := P) {y : P | False}
Tactic: simp only [h, not_sSameSide_bot]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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.SSameSide x y}
have pos : ∀ (hx : x ∈ s), IsPreconnected.{u_4} (α := P) {y : P | s.SSameSide x y}
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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}
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SSameSide x y}
have neg : ∀ (hx : x ∉ s), IsPreconnected.{u_4} (α := P) {y : P | s.SSameSide x y}
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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}
have pos : IsPreconnected.{u_4} (α := P) {y : P | False}
Tactic: simp only [hx, SSameSide, not_true, false_and, and_false]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ IsConnected.{u_4} (α := P) {y : P | s.WOppSide x y}
have obtain : ∀ (p : P) (hp : p ∈ (↑s : Set P)), IsConnected.{u_4} (α := P) {y : P | s.WOppSide x y}
Tactic: obtain ⟨p, hp⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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)
⊢ IsConnected.{u_4} (α := P) {y : P | s.WOppSide x y}
have this : Nonempty.{u_4 + 1} ↥s
Tactic: haveI : Nonempty s := ⟨⟨p, hp⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ IsConnected.{u_4} (α := P) {y : P | s.WOppSide x y}
have pos : ∀ (hx : x ∈ s), IsConnected.{u_4} (α := P) {y : P | s.WOppSide x y}
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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}
⊢ IsConnected.{u_4} (α := P) {y : P | s.WOppSide x y}
have neg : ∀ (hx : x ∉ s), IsConnected.{u_4} (α := P) {y : P | s.WOppSide x y}
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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.{u_4} (α := P) {y : P | s.WOppSide x y}
have pos : IsConnected.{u_4} (α := P) {y : P | True}
Tactic: simp only [wOppSide_of_left_mem, hx]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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.{u_4} (α := P) {y : P | s.WOppSide x y}
have neg : IsConnected (α := P)
  ((fun (x_1 : ℝ × P) ↦ x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' SProd.sprod (α := Set ℝ) (Set.Iic 0) (↑s : Set P))
Tactic: rw [setOf_wOppSide_eq_image2 hx hp, ← Set.image_prod]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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))
have neg : ConnectedSpace.{u_4} (↑(↑s : Set P) : Type u_4)
Tactic: refine (isConnected_Iic.prod (isConnected_iff_connectedSpace.2 ?_)).image _
      ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.WOppSide x y}
have inl : ∀ (h : (↑s : Set P) = ∅), IsPreconnected.{u_4} (α := P) {y : P | s.WOppSide x y}
Tactic: rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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}
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.WOppSide x y}
have inr : ∀ (h : (↑s : Set P).Nonempty), IsPreconnected.{u_4} (α := P) {y : P | s.WOppSide x y}
Tactic: rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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) = ∅
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.WOppSide x y}
have h₁ : s = ⊥
Tactic: rw [coe_eq_bot_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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 | s.WOppSide x y}
have inl : IsPreconnected.{u_4} (α := P) {y : P | False}
Tactic: simp only [h, not_wOppSide_bot]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ IsConnected.{u_4} (α := P) {y : P | s.SOppSide x y}
have obtain : ∀ (p : P) (hp : p ∈ (↑s : Set P)), IsConnected.{u_4} (α := P) {y : P | s.SOppSide x y}
Tactic: obtain ⟨p, hp⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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)
⊢ IsConnected.{u_4} (α := P) {y : P | s.SOppSide x y}
have this : Nonempty.{u_4 + 1} ↥s
Tactic: haveI : Nonempty s := ⟨⟨p, hp⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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.{u_4} (α := P) {y : P | s.SOppSide x y}
have rw : IsConnected (α := P)
  ((fun (x_1 : ℝ × P) ↦ x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' SProd.sprod (α := Set ℝ) (Set.Iio 0) (↑s : Set P))
Tactic: rw [setOf_sOppSide_eq_image2 hx hp, ← Set.image_prod]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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))
have refine : ConnectedSpace.{u_4} (↑(↑s : Set P) : Type u_4)
Tactic: refine (isConnected_Iio.prod (isConnected_iff_connectedSpace.2 ?_)).image _
    ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SOppSide x y}
have inl : ∀ (h : (↑s : Set P) = ∅), IsPreconnected.{u_4} (α := P) {y : P | s.SOppSide x y}
Tactic: rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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}
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SOppSide x y}
have inr : ∀ (h : (↑s : Set P).Nonempty), IsPreconnected.{u_4} (α := P) {y : P | s.SOppSide x y}
Tactic: rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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) = ∅
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SOppSide x y}
have h₁ : s = ⊥
Tactic: rw [coe_eq_bot_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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 | s.SOppSide x y}
have inl : IsPreconnected.{u_4} (α := P) {y : P | False}
Tactic: simp only [h, not_sOppSide_bot]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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.SOppSide x y}
have pos : ∀ (hx : x ∈ s), IsPreconnected.{u_4} (α := P) {y : P | s.SOppSide x y}
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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.SOppSide x y}
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SOppSide x y}
have neg : ∀ (hx : x ∉ s), IsPreconnected.{u_4} (α := P) {y : P | s.SOppSide x y}
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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.SOppSide x y}
have pos : IsPreconnected.{u_4} (α := P) {y : P | False}
Tactic: simp only [hx, SOppSide, not_true, false_and, and_false]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
h0 : w₁ i ≠ 0
⊢ SSameSide (affineSpan R (Set.range (s.faceOpposite i).points))
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂)
have h0' : w₂ i ≠ 0
Tactic: have h0' : w₂ i ≠ 0 := by intro h; simp_all
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
⊢ SSameSide (affineSpan R (Set.range (s.faceOpposite i).points))
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂)
have refine : WSameSide (affineSpan R (Set.range (s.faceOpposite i).points))
  ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁)
  ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂)
Tactic: refine ⟨?_, (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₁).not.2 h0,
    (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₂).not.2 h0'⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
⊢ WSameSide (affineSpan R (Set.range (s.faceOpposite i).points))
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂)
have obtain : ∀ (j : Fin (n + 1)) (hj : j ≠ i),
  WSameSide (affineSpan R (Set.range (s.faceOpposite i).points))
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂)
Tactic: obtain ⟨j, hj⟩ : ∃ j, j ≠ i := exists_ne _