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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
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
hy : y ∉ s
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
hy : y ∉ s
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
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : y = p₂
⊢ ∃ (a : R), 0 < a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
False.elim (hy (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
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : y = p₂
⊢ ∃ (a : R), 0 < a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
exact False.elim (hy (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
hy : y ∉ s
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₂, p₂, hp₂, ?_⟩

Premises used: HDiv.hDiv, 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
hy : y ∉ s
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₂, 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
hy : y ∉ s
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.SSameSide x (t • (x -ᵥ p) +ᵥ p')

Tactic:
sSameSide_smul_vsub_vadd_right hx hp hp' ht

Premises used: AffineSubspace.sSameSide_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.SSameSide x (t • (x -ᵥ p) +ᵥ p')

Tactic:
exact sSameSide_smul_vsub_vadd_right hx hp hp' ht

Premises used: AffineSubspace.sSameSide_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.WOppSide x y} y ↔
      Membership.mem (γ := Set P) (Set.image2 (fun (t : R) (q : P) ↦ t • (x -ᵥ p) +ᵥ q) (Set.Iic 0) (↑s : Set P)) y
⊢ Eq (α := Set P) {y : P | s.WOppSide x y}
    (Set.image2 (fun (t : R) (q : P) ↦ t • (x -ᵥ p) +ᵥ q) (Set.Iic 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.WOppSide x y ↔ ∃ a ≤ 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
⊢ Membership.mem (γ := Set P) {y : P | s.WOppSide x y} y ↔
    Membership.mem (γ := Set P) (Set.image2 (fun (t : R) (q : P) ↦ t • (x -ᵥ p) +ᵥ q) (Set.Iic 0) (↑s : Set P)) y

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

Premises used: Set.mem_image2, Set.mem_setOf, Set.mem_Iic
-- 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.WOppSide x y → ∃ a ≤ 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
h₁ : (∃ a ≤ 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y) → s.WOppSide x y
⊢ s.WOppSide x y ↔ ∃ a ≤ 0, ∃ 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) (p₂ -ᵥ y)) → ∃ a ≤ 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
⊢ s.WOppSide x y → ∃ a ≤ 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
rw [wOppSide_iff_exists_left hp, or_iff_right hx]

Premises used: AffineSubspace.wOppSide_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
⊢ ∃ a ≤ 0, ∃ 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 ≤ 0, ∃ 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 : p₂ -ᵥ y = 0
⊢ p₂ = y

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 : p₂ = y
⊢ ∃ a ≤ 0, ∃ 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 : p₂ = y
h₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x -ᵥ p) +ᵥ p₂ = y
⊢ ∃ a ≤ 0, ∃ 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 : p₂ = y
⊢ 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₂ • (p₂ -ᵥ y)
⊢ ∃ a ≤ 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
⟨-r₁ / r₂, (div_neg_of_neg_of_pos (Left.neg_neg_iff.2 hr₁) hr₂).le, p₂, hp₂, ?_⟩

Premises used: Iff.mpr, Left.neg_neg_iff, HDiv.hDiv, LT.lt.le, And.intro, Exists.intro, div_neg_of_neg_of_pos, Neg.neg
-- 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₂ • (p₂ -ᵥ y)
h₁ : (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
⊢ ∃ a ≤ 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
refine ⟨-r₁ / r₂, (div_neg_of_neg_of_pos (Left.neg_neg_iff.2 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₂ • (p₂ -ᵥ y)
h₁ : (r₂⁻¹ * -r₁) • (x -ᵥ p) +ᵥ p₂ = y
h₂ : r₂⁻¹ • -r₁ • (x -ᵥ p) +ᵥ p₂ = y
h₃ : r₂⁻¹ • -(r₁ • (x -ᵥ p)) +ᵥ p₂ = y
h₄ : r₂⁻¹ • -(r₂ • (p₂ -ᵥ y)) +ᵥ p₂ = y
h₅ : -(r₂⁻¹ • r₂ • (p₂ -ᵥ y)) +ᵥ p₂ = y
h₆ : -((r₂⁻¹ * r₂) • (p₂ -ᵥ y)) +ᵥ p₂ = y
h₇ : -HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (p₂ -ᵥ y) +ᵥ p₂ = y
h₈ : -(p₂ -ᵥ y) +ᵥ 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, neg_smul, h, smul_neg, smul_smul,
        inv_mul_cancel₀ hr₂.ne.symm, one_smul, neg_vsub_eq_vsub_rev, vsub_vadd]

Premises used: neg_smul, smul_smul, smul_neg, Ne.symm, one_smul, neg_vsub_eq_vsub_rev, 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 : t ≤ 0
p' : P
hp' : p' ∈ (↑s : Set P)
⊢ s.WOppSide x (t • (x -ᵥ p) +ᵥ p')

Tactic:
wOppSide_smul_vsub_vadd_right x hp hp' ht

Premises used: AffineSubspace.wOppSide_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 : t ≤ 0
p' : P
hp' : p' ∈ (↑s : Set P)
⊢ s.WOppSide x (t • (x -ᵥ p) +ᵥ p')

Tactic:
exact wOppSide_smul_vsub_vadd_right x hp hp' ht

Premises used: AffineSubspace.wOppSide_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.SOppSide x y} y ↔
      Membership.mem (γ := Set P) (Set.image2 (fun (t : R) (q : P) ↦ t • (x -ᵥ p) +ᵥ q) (Set.Iio 0) (↑s : Set P)) y
⊢ Eq (α := Set P) {y : P | s.SOppSide x y}
    (Set.image2 (fun (t : R) (q : P) ↦ t • (x -ᵥ p) +ᵥ q) (Set.Iio 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.SOppSide x y ↔ ∃ a < 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
⊢ Membership.mem (γ := Set P) {y : P | s.SOppSide x y} y ↔
    Membership.mem (γ := Set P) (Set.image2 (fun (t : R) (q : P) ↦ t • (x -ᵥ p) +ᵥ q) (Set.Iio 0) (↑s : Set P)) y

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

Premises used: Set.mem_Iio, Set.mem_image2, 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.SOppSide x y → ∃ a < 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
h₁ : (∃ a < 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y) → s.SOppSide x y
⊢ s.SOppSide x y ↔ ∃ a < 0, ∃ 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) (p₂ -ᵥ y)) → ∃ a < 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
⊢ s.SOppSide x y → ∃ a < 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
rw [sOppSide_iff_exists_left hp]

Premises used: AffineSubspace.sOppSide_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
⊢ ∃ a < 0, ∃ 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
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : x = p
⊢ ∃ a < 0, ∃ 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
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : p₂ -ᵥ y = 0
⊢ p₂ = y

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
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : p₂ = y
⊢ ∃ a < 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
False.elim (hy (h ▸ hp₂))

Premises used: False.elim, Eq.rec
-- 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 : p₂ = y
⊢ ∃ a < 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
exact False.elim (hy (h ▸ hp₂))

Premises used: False.elim, Eq.rec
-- 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
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (p₂ -ᵥ y)
⊢ ∃ a < 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
⟨-r₁ / r₂, div_neg_of_neg_of_pos (Left.neg_neg_iff.2 hr₁) hr₂, p₂, hp₂, ?_⟩

Premises used: Iff.mpr, Left.neg_neg_iff, HDiv.hDiv, And.intro, Exists.intro, div_neg_of_neg_of_pos, Neg.neg
-- 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
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (p₂ -ᵥ y)
h₁ : (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
⊢ ∃ a < 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y

Tactic:
refine ⟨-r₁ / r₂, div_neg_of_neg_of_pos (Left.neg_neg_iff.2 hr₁) hr₂, 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
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (p₂ -ᵥ y)
h₁ : (r₂⁻¹ * -r₁) • (x -ᵥ p) +ᵥ p₂ = y
h₂ : r₂⁻¹ • -r₁ • (x -ᵥ p) +ᵥ p₂ = y
h₃ : r₂⁻¹ • -(r₁ • (x -ᵥ p)) +ᵥ p₂ = y
h₄ : r₂⁻¹ • -(r₂ • (p₂ -ᵥ y)) +ᵥ p₂ = y
h₅ : -(r₂⁻¹ • r₂ • (p₂ -ᵥ y)) +ᵥ p₂ = y
h₆ : -((r₂⁻¹ * r₂) • (p₂ -ᵥ y)) +ᵥ p₂ = y
h₇ : -HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (p₂ -ᵥ y) +ᵥ p₂ = y
h₈ : -(p₂ -ᵥ y) +ᵥ 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, neg_smul, h, smul_neg, smul_smul,
        inv_mul_cancel₀ hr₂.ne.symm, one_smul, neg_vsub_eq_vsub_rev, vsub_vadd]

Premises used: neg_smul, smul_smul, smul_neg, Ne.symm, one_smul, neg_vsub_eq_vsub_rev, 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 : t < 0
p' : P
hp' : p' ∈ (↑s : Set P)
⊢ s.SOppSide x (t • (x -ᵥ p) +ᵥ p')

Tactic:
sOppSide_smul_vsub_vadd_right hx hp hp' ht

Premises used: AffineSubspace.sOppSide_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 : t < 0
p' : P
hp' : p' ∈ (↑s : Set P)
⊢ s.SOppSide x (t • (x -ᵥ p) +ᵥ p')

Tactic:
exact sOppSide_smul_vsub_vadd_right hx hp hp' ht

Premises used: AffineSubspace.sOppSide_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 y : P
hx : x ∈ s
⊢ s.WOppSide y ((pointReflection R x : (a : P) → P) y)

Tactic:
(wbtw_pointReflection R _ _).wOppSide₁₃ hx

Premises used: Wbtw.wOppSide₁₃, wbtw_pointReflection
-- 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
⊢ s.SOppSide y ((pointReflection R x : (a : P) → P) y)

Tactic:
(sbtw_pointReflection_of_ne R fun h => hy ?_).sOppSide_of_notMem_of_mem hy hx

Premises used: sbtw_pointReflection_of_ne, Sbtw.sOppSide_of_notMem_of_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 y : P
hx : x ∈ s
hy : y ∉ s
refine : ∀ (h : x = y), y ∈ s
⊢ s.SOppSide y ((pointReflection R x : (a : P) → P) y)

Tactic:
refine (sbtw_pointReflection_of_ne R fun h => hy ?_).sOppSide_of_notMem_of_mem hy hx

Premises used: sbtw_pointReflection_of_ne, Sbtw.sOppSide_of_notMem_of_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 y : P
hx : x ∈ s
hy : y ∉ s
h : x = y
rwa rwa₁ rwa₂ rwa₃ : x ∈ s
⊢ y ∈ s

Tactic:
rwa [← 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
h : (↑s : Set P).Nonempty
obtain : ∀ (p : P) (hp : p ∈ (↑s : Set P)), IsConnected.{u_4} (α := P) {y : P | s.WSameSide x y}
⊢ IsConnected.{u_4} (α := P) {y : P | s.WSameSide 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)
⊢ 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 : 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}
neg : ∀ (hx : x ∉ s), IsConnected.{u_4} (α := P) {y : P | s.WSameSide x y}
⊢ IsConnected.{u_4} (α := P) {y : P | s.WSameSide x y}

Tactic:
by_cases hx : x ∈ s