awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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
⊢ x ∈ s
have rwa₂ : ∀ (h : 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
Cleared hypotheses: h
-- 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 : 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
have refine : ∀ (h : t • (x -ᵥ p₁) +ᵥ p₂ ∈ s), x ∈ s
Tactic: refine ⟨wOppSide_smul_vsub_vadd_left x hp₁ hp₂ ht.le, fun h => hx ?_, hx⟩
-- 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 : 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
⊢ x ∈ s
have rwa : ∀ (h : t • (x -ᵥ p₁) ∈ s.direction), 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
Cleared hypotheses: h
-- 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 : 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
⊢ x ∈ s
have rwa₁ : ∀ (h : x -ᵥ p₁ ∈ s.direction), 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
Cleared hypotheses: h
-- 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 : 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
⊢ x ∈ s
have rwa₂ : ∀ (h : 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
Cleared hypotheses: h
-- 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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
⊢ 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))
have 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
Tactic: ext y
-- 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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
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
have h : s.WSameSide x y ↔ ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
Tactic: simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Ici]
-- 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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ s.WSameSide x y ↔ ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
have h : s.WSameSide x y → ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
Tactic: constructor
-- 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 : 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
⊢ s.WSameSide x y ↔ ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
have h₁ : (∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y) → s.WSameSide x y
Tactic: constructor
-- 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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ s.WSameSide x y → ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
have h : (∃ p₂ ∈ s, SameRay R (x -ᵥ p) (y -ᵥ p₂)) → ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
Tactic: rw [wSameSide_iff_exists_left hp, or_iff_right hx]
-- 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 : 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
⊢ ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
have h₁ : x = p
Tactic: rw [vsub_eq_zero_iff_eq] at h
Cleared hypotheses: h
-- 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 : 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
⊢ ∃ (a : R), 0 ≤ a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
have h₁ : y = p₂
Tactic: rw [vsub_eq_zero_iff_eq] at h
Cleared hypotheses: h
-- 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 : 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
have h₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x -ᵥ p) +ᵥ p₂ = y
Tactic: refine ⟨0, le_rfl, p₂, hp₂, ?_⟩
-- 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 : 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
have h₁ : (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
Tactic: refine ⟨r₁ / r₂, (div_pos hr₁ hr₂).le, p₂, hp₂, ?_⟩
-- 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 : 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₂)
⊢ (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₁ : (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]
-- 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 : 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
⊢ (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₂ : 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]
-- 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 : 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
⊢ (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₃ : r₂⁻¹ • r₂ • (y -ᵥ p₂) +ᵥ p₂ = y
Tactic: rw [div_eq_inv_mul, ← smul_smul, h, smul_smul, inv_mul_cancel₀ hr₂.ne.symm, one_smul,
        vsub_vadd]
-- 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 : 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
⊢ (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₄ : (r₂⁻¹ * r₂) • (y -ᵥ p₂) +ᵥ p₂ = y
Tactic: rw [div_eq_inv_mul, ← smul_smul, h, smul_smul, inv_mul_cancel₀ hr₂.ne.symm, one_smul,
        vsub_vadd]
-- 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 : 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
⊢ (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₅ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (y -ᵥ p₂) +ᵥ p₂ = y
Tactic: rw [div_eq_inv_mul, ← smul_smul, h, smul_smul, inv_mul_cancel₀ hr₂.ne.symm, one_smul,
        vsub_vadd]
-- 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 : 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
⊢ (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₆ : (y -ᵥ p₂) +ᵥ p₂ = y
Tactic: rw [div_eq_inv_mul, ← smul_smul, h, smul_smul, inv_mul_cancel₀ hr₂.ne.symm, one_smul,
        vsub_vadd]
-- 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 : 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
⊢ (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₇ : y = y
Tactic: rw [div_eq_inv_mul, ← smul_smul, h, smul_smul, inv_mul_cancel₀ hr₂.ne.symm, one_smul,
        vsub_vadd]
-- 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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
⊢ 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))
have 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
Tactic: ext y
-- 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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
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
have h : s.SSameSide x y ↔ ∃ (a : R), 0 < a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
Tactic: simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Ioi]
-- 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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ s.SSameSide x y ↔ ∃ (a : R), 0 < a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
have h : s.SSameSide x y → ∃ (a : R), 0 < a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
Tactic: constructor
-- 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 : 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
⊢ s.SSameSide x y ↔ ∃ (a : R), 0 < a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
have h₁ : (∃ (a : R), 0 < a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y) → s.SSameSide x y
Tactic: constructor
-- 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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ s.SSameSide x y → ∃ (a : R), 0 < a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
have 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
Tactic: rw [sSameSide_iff_exists_left hp]
-- 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 : 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
⊢ ∃ (a : R), 0 < a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
have h₁ : x = p
Tactic: rw [vsub_eq_zero_iff_eq] at h
Cleared hypotheses: h
-- 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 : 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
⊢ ∃ (a : R), 0 < a ∧ ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
have h₁ : y = p₂
Tactic: rw [vsub_eq_zero_iff_eq] at h
Cleared hypotheses: h
-- 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 : 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
have h₁ : (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
Tactic: refine ⟨r₁ / r₂, div_pos hr₁ hr₂, p₂, hp₂, ?_⟩
-- 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 : 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₂)
⊢ (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₁ : (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]
-- 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 : 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
⊢ (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₂ : 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]
-- 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 : 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
⊢ (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₃ : r₂⁻¹ • r₂ • (y -ᵥ p₂) +ᵥ p₂ = y
Tactic: rw [div_eq_inv_mul, ← smul_smul, h, smul_smul, inv_mul_cancel₀ hr₂.ne.symm, one_smul,
        vsub_vadd]
-- 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 : 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
⊢ (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₄ : (r₂⁻¹ * r₂) • (y -ᵥ p₂) +ᵥ p₂ = y
Tactic: rw [div_eq_inv_mul, ← smul_smul, h, smul_smul, inv_mul_cancel₀ hr₂.ne.symm, one_smul,
        vsub_vadd]
-- 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 : 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
⊢ (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₅ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (y -ᵥ p₂) +ᵥ p₂ = y
Tactic: rw [div_eq_inv_mul, ← smul_smul, h, smul_smul, inv_mul_cancel₀ hr₂.ne.symm, one_smul,
        vsub_vadd]
-- 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 : 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
⊢ (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₆ : (y -ᵥ p₂) +ᵥ p₂ = y
Tactic: rw [div_eq_inv_mul, ← smul_smul, h, smul_smul, inv_mul_cancel₀ hr₂.ne.symm, one_smul,
        vsub_vadd]
-- 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 : 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
⊢ (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₇ : y = y
Tactic: rw [div_eq_inv_mul, ← smul_smul, h, smul_smul, inv_mul_cancel₀ hr₂.ne.symm, one_smul,
        vsub_vadd]
-- 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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
⊢ 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))
have 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
Tactic: ext y
-- 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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
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
have h : s.WOppSide x y ↔ ∃ a ≤ 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
Tactic: simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Iic]
-- 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 : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ s.WOppSide x y ↔ ∃ a ≤ 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
have h : s.WOppSide x y → ∃ a ≤ 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
Tactic: constructor
-- 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 : 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
⊢ s.WOppSide x y ↔ ∃ a ≤ 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
have h₁ : (∃ a ≤ 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y) → s.WOppSide x y
Tactic: constructor