awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x y z : P
h : Sbtw R x y z
hx : x ∉ s
hy : y ∈ s
⊢ s.SOppSide x z

Tactic:
⟨h.wbtw.wOppSide₁₃ hy, hx, fun hz => hx ?_⟩

Premises used: Wbtw.wOppSide₁₃, And.intro, AffineSubspace.SOppSide, Sbtw.wbtw
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x y z : P
h : Sbtw R x y z
hx : x ∉ s
hy : y ∈ s
refine : ∀ (hz : z ∈ s), x ∈ s
⊢ s.SOppSide x z

Tactic:
refine ⟨h.wbtw.wOppSide₁₃ hy, hx, fun hz => hx ?_⟩
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x y z : P
h : Sbtw R x y z
hx : x ∉ s
hy : y ∈ s
hz : z ∈ s
rcases :
  ∀ (t : R) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) (hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) t : P))
    (hyx : (lineMap x z : (a : R) → P) t ≠ x) (hyz : (lineMap x z : (a : R) → P) t ≠ z), x ∈ s
⊢ x ∈ s

Tactic:
rcases h with ⟨⟨t, ⟨ht0, ht1⟩, rfl⟩, hyx, hyz⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x z : P
hx : x ∉ s
hz : z ∈ s
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) t : P)
hyx : (lineMap x z : (a : R) → P) t ≠ x
hyz : (lineMap x z : (a : R) → P) t ≠ z
⊢ t • (z -ᵥ x) +ᵥ x ∈ s

Tactic:
rw [lineMap_apply] at hy

Premises used: AffineMap.lineMap_apply
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x z : P
hx : x ∉ s
hz : z ∈ s
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) t : P)
hyx : (lineMap x z : (a : R) → P) t ≠ x
hyz : (lineMap x z : (a : R) → P) t ≠ z
hy₁ : t • (z -ᵥ x) +ᵥ x ∈ s
⊢ (lineMap x z : (a : R) → P) t ≠ x

Tactic:
rw [lineMap_apply] at hy

Premises used: AffineMap.lineMap_apply
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x z : P
hx : x ∉ s
hz : z ∈ s
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : Membership.mem (α := P) s ((lineMap x z : (a : R) → P) t : P)
hyx : (lineMap x z : (a : R) → P) t ≠ x
hyz : (lineMap x z : (a : R) → P) t ≠ z
hy₁ : t • (z -ᵥ x) +ᵥ x ∈ s
hyx₁ : (lineMap x z : (a : R) → P) t ≠ x
⊢ (lineMap x z : (a : R) → P) t ≠ z

Tactic:
rw [lineMap_apply] at hy

Premises used: AffineMap.lineMap_apply
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x z : P
hx : x ∉ s
hz : z ∈ s
ht0 : LE.le.{u_1} (α := R) 0 1
ht1 : LE.le.{u_1} (α := R) 1 1
hy : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (z -ᵥ x) +ᵥ x ∈ s
hyx : (lineMap x z : (a : R) → P) 1 ≠ x
hyz : (lineMap x z : (a : R) → P) 1 ≠ z
⊢ False

Tactic:
simp [lineMap_apply] at hyz

Premises used: AffineMap.lineMap_apply
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x z : P
hx : x ∉ s
hz : z ∈ s
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : t • (z -ᵥ x) +ᵥ x ∈ s
hyx : (lineMap x z : (a : R) → P) t ≠ x
hyz : (lineMap x z : (a : R) → P) t ≠ z
⊢ t ≠ 1

Tactic:
have ht : t ≠ 1 := by
    rintro rfl
    simp [lineMap_apply] at hyz
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x z : P
hx : x ∉ s
hz : z ∈ s
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : t • (z -ᵥ x) +ᵥ x ∈ s
hyx : (lineMap x z : (a : R) → P) t ≠ x
hyz : (lineMap x z : (a : R) → P) t ≠ z
ht : t ≠ 1
⊢ (t • (z -ᵥ x) +ᵥ x) -ᵥ z ∈ s.direction

Tactic:
have hy' := vsub_mem_direction hy hz
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x z : P
hx : x ∉ s
hz : z ∈ s
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : t • (z -ᵥ x) +ᵥ x ∈ s
hyx : (lineMap x z : (a : R) → P) t ≠ x
hyz : (lineMap x z : (a : R) → P) t ≠ z
ht : t ≠ 1
hy' : (t • (z -ᵥ x) +ᵥ x) -ᵥ z ∈ s.direction
⊢ z -ᵥ x ∈ s.direction

Tactic:
rw [vadd_vsub_assoc, ← neg_vsub_eq_vsub_rev z, ← neg_one_smul R (z -ᵥ x), ← add_smul,
    ← sub_eq_add_neg, s.direction.smul_mem_iff (sub_ne_zero_of_ne ht)] at hy'

Premises used: vadd_vsub_assoc, neg_one_smul, sub_eq_add_neg, VSub.vsub, add_smul, sub_ne_zero_of_ne, Submodule.smul_mem_iff, neg_vsub_eq_vsub_rev, AffineSubspace.direction
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x z : P
hx : x ∉ s
hz : z ∈ s
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : t • (z -ᵥ x) +ᵥ x ∈ s
hyx : (lineMap x z : (a : R) → P) t ≠ x
hyz : (lineMap x z : (a : R) → P) t ≠ z
ht : t ≠ 1
hy' : z -ᵥ x ∈ s.direction
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hy : x ∈ s) (hyx : (lineMap x z : (a : R) → P) t ≠ x) (hyz : (lineMap x z : (a : R) → P) t ≠ z) (ht : t ≠ 1)
    (hy' : z -ᵥ x ∈ s.direction), x ∈ s
⊢ x ∈ s

Tactic:
rwa [vadd_mem_iff_mem_of_mem_direction (Submodule.smul_mem _ _ hy')] at hy

Premises used: AffineSubspace.vadd_mem_iff_mem_of_mem_direction, Submodule.smul_mem
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p₁ p₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 < t
⊢ s.SSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
⟨wSameSide_smul_vsub_vadd_left x hp₁ hp₂ ht.le, fun h => hx ?_, hx⟩

Premises used: AffineSubspace.SSameSide, LT.lt.le, AffineSubspace.wSameSide_smul_vsub_vadd_left, And.intro
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p₁ p₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 < t
refine : ∀ (h : t • (x -ᵥ p₁) +ᵥ p₂ ∈ s), x ∈ s
⊢ s.SSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
refine ⟨wSameSide_smul_vsub_vadd_left x hp₁ hp₂ ht.le, fun h => hx ?_, hx⟩
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p₁ p₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 < t
h : t • (x -ᵥ p₁) +ᵥ p₂ ∈ s
rwa : ∀ (h : t • (x -ᵥ p₁) ∈ s.direction), x ∈ s
rwa₁ : ∀ (h : x -ᵥ p₁ ∈ s.direction), x ∈ s
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : x ∈ s), x ∈ s
⊢ x ∈ s

Tactic:
rwa [vadd_mem_iff_mem_direction _ hp₂, s.direction.smul_mem_iff ht.ne.symm,
    vsub_right_mem_direction_iff_mem hp₁] at h

Premises used: Ne.symm, Submodule.smul_mem_iff, AffineSubspace.vadd_mem_iff_mem_direction, AffineSubspace.vsub_right_mem_direction_iff_mem, AffineSubspace.direction, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p₁ p₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 < t
⊢ s.SSameSide x (t • (x -ᵥ p₁) +ᵥ p₂)

Tactic:
(sSameSide_smul_vsub_vadd_left hx hp₁ hp₂ ht).symm

Premises used: AffineSubspace.SSameSide.symm, AffineSubspace.sSameSide_smul_vsub_vadd_left
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
hy : y ∉ s
t : R
ht : 0 < t
⊢ s.SSameSide ((lineMap x y : (a : R) → P) t) y

Tactic:
sSameSide_smul_vsub_vadd_left hy hx hx ht

Premises used: AffineSubspace.sSameSide_smul_vsub_vadd_left
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
hy : y ∉ s
t : R
ht : 0 < t
⊢ s.SSameSide y ((lineMap x y : (a : R) → P) t)

Tactic:
(sSameSide_lineMap_left hx hy ht).symm

Premises used: AffineSubspace.SSameSide.symm, AffineSubspace.sSameSide_lineMap_left
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p₁ p₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t < 0
⊢ s.SOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
⟨wOppSide_smul_vsub_vadd_left x hp₁ hp₂ ht.le, fun h => hx ?_, hx⟩

Premises used: AffineSubspace.wOppSide_smul_vsub_vadd_left, LT.lt.le, And.intro, AffineSubspace.SOppSide
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p₁ p₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t < 0
refine : ∀ (h : t • (x -ᵥ p₁) +ᵥ p₂ ∈ s), x ∈ s
⊢ s.SOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
refine ⟨wOppSide_smul_vsub_vadd_left x hp₁ hp₂ ht.le, fun h => hx ?_, hx⟩
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p₁ p₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t < 0
h : t • (x -ᵥ p₁) +ᵥ p₂ ∈ s
rwa : ∀ (h : t • (x -ᵥ p₁) ∈ s.direction), x ∈ s
rwa₁ : ∀ (h : x -ᵥ p₁ ∈ s.direction), x ∈ s
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : x ∈ s), x ∈ s
⊢ x ∈ s

Tactic:
rwa [vadd_mem_iff_mem_direction _ hp₂, s.direction.smul_mem_iff ht.ne,
    vsub_right_mem_direction_iff_mem hp₁] at h

Premises used: Submodule.smul_mem_iff, AffineSubspace.vadd_mem_iff_mem_direction, AffineSubspace.vsub_right_mem_direction_iff_mem, AffineSubspace.direction, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p₁ p₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t < 0
⊢ s.SOppSide x (t • (x -ᵥ p₁) +ᵥ p₂)

Tactic:
(sOppSide_smul_vsub_vadd_left hx hp₁ hp₂ ht).symm

Premises used: AffineSubspace.SOppSide.symm, AffineSubspace.sOppSide_smul_vsub_vadd_left
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
hy : y ∉ s
t : R
ht : t < 0
⊢ s.SOppSide ((lineMap x y : (a : R) → P) t) y

Tactic:
sOppSide_smul_vsub_vadd_left hy hx hx ht

Premises used: AffineSubspace.sOppSide_smul_vsub_vadd_left
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
hy : y ∉ s
t : R
ht : t < 0
⊢ s.SOppSide y ((lineMap x y : (a : R) → P) t)

Tactic:
(sOppSide_lineMap_left hx hy ht).symm

Premises used: AffineSubspace.SOppSide.symm, AffineSubspace.sOppSide_lineMap_left
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
h :
  ∀ (y : P),
    Membership.mem (γ := Set P) {y : P | s.WSameSide x y} y ↔
      Membership.mem (γ := Set P) (Set.image2 (fun (t : R) (q : P) ↦ t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) (↑s : Set P)) y
⊢ Eq (α := Set P) {y : P | s.WSameSide x y}
    (Set.image2 (fun (t : R) (q : P) ↦ t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) (↑s : Set P))

Tactic:
ext y
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
h : s.WSameSide x y ↔ ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
⊢ Membership.mem (γ := Set P) {y : P | s.WSameSide x y} y ↔
    Membership.mem (γ := Set P) (Set.image2 (fun (t : R) (q : P) ↦ t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) (↑s : Set P)) y

Tactic:
simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Ici]

Premises used: Set.mem_image2, Set.mem_setOf, Set.mem_Ici
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
h : s.WSameSide x y → ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
h₁ : (∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y) → s.WSameSide x y
⊢ s.WSameSide x y ↔ ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
h : (∃ p₂ ∈ s, SameRay R (x -ᵥ p) (y -ᵥ p₂)) → ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
⊢ s.WSameSide x y → ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
rw [wSameSide_iff_exists_left hp, or_iff_right hx]

Premises used: AffineSubspace.wSameSide_iff_exists_left, or_iff_right
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : x -ᵥ p = 0
⊢ x = p

Tactic:
rw [vsub_eq_zero_iff_eq] at h

Premises used: vsub_eq_zero_iff_eq
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : x = p
⊢ ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
False.elim (hx (h.symm ▸ hp))

Premises used: False.elim, Eq.rec, Eq.symm
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : x = p
⊢ ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
exact False.elim (hx (h.symm ▸ hp))

Premises used: False.elim, Eq.rec, Eq.symm
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : y -ᵥ p₂ = 0
⊢ y = p₂

Tactic:
rw [vsub_eq_zero_iff_eq] at h

Premises used: vsub_eq_zero_iff_eq
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : y = p₂
⊢ ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
⟨0, le_rfl, p₂, hp₂, ?_⟩

Premises used: le_rfl, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : y = p₂
h₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x -ᵥ p) +ᵥ p₂ = y
⊢ ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
refine ⟨0, le_rfl, p₂, hp₂, ?_⟩
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : y = p₂
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x -ᵥ p) +ᵥ p₂ = y

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (y -ᵥ p₂)
⊢ ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
⟨r₁ / r₂, (div_pos hr₁ hr₂).le, p₂, hp₂, ?_⟩

Premises used: HDiv.hDiv, LT.lt.le, And.intro, Exists.intro, div_pos
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (y -ᵥ p₂)
h₁ : (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
⊢ ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
refine ⟨r₁ / r₂, (div_pos hr₁ hr₂).le, p₂, hp₂, ?_⟩
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (y -ᵥ p₂)
h₁ : (r₂⁻¹ * r₁) • (x -ᵥ p) +ᵥ p₂ = y
h₂ : r₂⁻¹ • r₁ • (x -ᵥ p) +ᵥ p₂ = y
h₃ : r₂⁻¹ • r₂ • (y -ᵥ p₂) +ᵥ p₂ = y
h₄ : (r₂⁻¹ * r₂) • (y -ᵥ p₂) +ᵥ p₂ = y
h₅ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (y -ᵥ p₂) +ᵥ p₂ = y
h₆ : (y -ᵥ p₂) +ᵥ p₂ = y
h₇ h₈ : y = y
⊢ (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y

Tactic:
rw [div_eq_inv_mul, ← smul_smul, h, smul_smul, inv_mul_cancel₀ hr₂.ne.symm, one_smul,
        vsub_vadd]

Premises used: smul_smul, Ne.symm, one_smul, vsub_vadd, div_eq_inv_mul, inv_mul_cancel₀, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
t : R
ht : 0 ≤ t
p' : P
hp' : p' ∈ (↑s : Set P)
⊢ s.WSameSide x (t • (x -ᵥ p) +ᵥ p')

Tactic:
wSameSide_smul_vsub_vadd_right x hp hp' ht

Premises used: AffineSubspace.wSameSide_smul_vsub_vadd_right
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
t : R
ht : 0 ≤ t
p' : P
hp' : p' ∈ (↑s : Set P)
⊢ s.WSameSide x (t • (x -ᵥ p) +ᵥ p')

Tactic:
exact wSameSide_smul_vsub_vadd_right x hp hp' ht

Premises used: AffineSubspace.wSameSide_smul_vsub_vadd_right
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
h :
  ∀ (y : P),
    Membership.mem (γ := Set P) {y : P | s.SSameSide x y} y ↔
      Membership.mem (γ := Set P) (Set.image2 (fun (t : R) (q : P) ↦ t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) (↑s : Set P)) y
⊢ Eq (α := Set P) {y : P | s.SSameSide x y}
    (Set.image2 (fun (t : R) (q : P) ↦ t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) (↑s : Set P))

Tactic:
ext y
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
h : s.SSameSide x y ↔ ∃ (a : R), 0 < a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
⊢ Membership.mem (γ := Set P) {y : P | s.SSameSide x y} y ↔
    Membership.mem (γ := Set P) (Set.image2 (fun (t : R) (q : P) ↦ t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) (↑s : Set P)) y

Tactic:
simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Ioi]

Premises used: Set.mem_image2, Set.mem_Ioi, Set.mem_setOf
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
h : s.SSameSide x y → ∃ (a : R), 0 < a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
h₁ : (∃ (a : R), 0 < a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y) → s.SSameSide x y
⊢ s.SSameSide x y ↔ ∃ (a : R), 0 < a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
h :
  (x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p) (y -ᵥ p₂)) →
    ∃ (a : R), 0 < a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
⊢ s.SSameSide x y → ∃ (a : R), 0 < a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
rw [sSameSide_iff_exists_left hp]

Premises used: AffineSubspace.sSameSide_iff_exists_left
-- Module: Mathlib.Analysis.Convex.Side
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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : x -ᵥ p = 0
⊢ x = p

Tactic:
rw [vsub_eq_zero_iff_eq] at h

Premises used: vsub_eq_zero_iff_eq