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
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 : (∃ p₂ ∈ s, SameRay R (x -ᵥ p) (p₂ -ᵥ y)) → ∃ a ≤ 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
Tactic: rw [wOppSide_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 ≤ 0, ∃ 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 : p₂ -ᵥ y = 0
⊢ ∃ a ≤ 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
have h₁ : p₂ = y
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 : p₂ = y
⊢ ∃ a ≤ 0, ∃ 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₂ • (p₂ -ᵥ y)
⊢ ∃ a ≤ 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
have h₁ : (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
Tactic: refine ⟨-r₁ / r₂, (div_neg_of_neg_of_pos (Left.neg_neg_iff.2 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₂ • (p₂ -ᵥ y)
⊢ (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₁ : (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]
-- 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₂ • (p₂ -ᵥ y)
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, neg_smul, h, smul_neg, smul_smul,
        inv_mul_cancel₀ hr₂.ne.symm, one_smul, neg_vsub_eq_vsub_rev, 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₂ • (p₂ -ᵥ y)
h₁ : (r₂⁻¹ * -r₁) • (x -ᵥ p) +ᵥ p₂ = y
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, neg_smul, h, smul_neg, smul_smul,
        inv_mul_cancel₀ hr₂.ne.symm, one_smul, neg_vsub_eq_vsub_rev, 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₂ • (p₂ -ᵥ y)
h₁ : (r₂⁻¹ * -r₁) • (x -ᵥ p) +ᵥ p₂ = y
h₂ : r₂⁻¹ • -r₁ • (x -ᵥ p) +ᵥ p₂ = y
h₃ : r₂⁻¹ • -(r₁ • (x -ᵥ p)) +ᵥ p₂ = y
⊢ (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₄ : r₂⁻¹ • -(r₂ • (p₂ -ᵥ y)) +ᵥ 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]
-- 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₂ • (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
⊢ (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₅ : -(r₂⁻¹ • r₂ • (p₂ -ᵥ y)) +ᵥ 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]
-- 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₂ • (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
⊢ (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₆ : -((r₂⁻¹ * r₂) • (p₂ -ᵥ y)) +ᵥ 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]
-- 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₂ • (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
⊢ (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₇ : -HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (p₂ -ᵥ y) +ᵥ 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]
-- 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₂ • (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
⊢ (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₈ : -(p₂ -ᵥ y) +ᵥ 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]
-- 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₂ • (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
⊢ (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₉ : (y -ᵥ 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]
-- 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₂ • (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
⊢ (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₁₀ : y = 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]
-- 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.SOppSide x y}
    (Set.image2 (fun (t : R) (q : P) ↦ t • (x -ᵥ p) +ᵥ q) (Set.Iio 0) (↑s : Set P))
have 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
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.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
have h : s.SOppSide x y ↔ ∃ a < 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
Tactic: simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Iio]
-- 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.SOppSide x y ↔ ∃ a < 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
have h : s.SOppSide 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.SOppSide x 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
have h₁ : (∃ a < 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y) → s.SOppSide 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.SOppSide x y → ∃ a < 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
have h : (x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p) (p₂ -ᵥ y)) → ∃ a < 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
Tactic: rw [sOppSide_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 < 0, ∃ 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 : p₂ -ᵥ y = 0
⊢ ∃ a < 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
have h₁ : p₂ = y
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₂ • (p₂ -ᵥ y)
⊢ ∃ a < 0, ∃ b ∈ (↑s : Set P), a • (x -ᵥ p) +ᵥ b = y
have h₁ : (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
Tactic: refine ⟨-r₁ / r₂, div_neg_of_neg_of_pos (Left.neg_neg_iff.2 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₂ • (p₂ -ᵥ y)
⊢ (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₁ : (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]
-- 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₂ • (p₂ -ᵥ y)
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, neg_smul, h, smul_neg, smul_smul,
        inv_mul_cancel₀ hr₂.ne.symm, one_smul, neg_vsub_eq_vsub_rev, 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₂ • (p₂ -ᵥ y)
h₁ : (r₂⁻¹ * -r₁) • (x -ᵥ p) +ᵥ p₂ = y
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, neg_smul, h, smul_neg, smul_smul,
        inv_mul_cancel₀ hr₂.ne.symm, one_smul, neg_vsub_eq_vsub_rev, 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₂ • (p₂ -ᵥ y)
h₁ : (r₂⁻¹ * -r₁) • (x -ᵥ p) +ᵥ p₂ = y
h₂ : r₂⁻¹ • -r₁ • (x -ᵥ p) +ᵥ p₂ = y
h₃ : r₂⁻¹ • -(r₁ • (x -ᵥ p)) +ᵥ p₂ = y
⊢ (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₄ : r₂⁻¹ • -(r₂ • (p₂ -ᵥ y)) +ᵥ 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]
-- 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₂ • (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
⊢ (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₅ : -(r₂⁻¹ • r₂ • (p₂ -ᵥ y)) +ᵥ 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]
-- 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₂ • (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
⊢ (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₆ : -((r₂⁻¹ * r₂) • (p₂ -ᵥ y)) +ᵥ 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]
-- 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₂ • (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
⊢ (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₇ : -HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (p₂ -ᵥ y) +ᵥ 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]
-- 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₂ • (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
⊢ (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₈ : -(p₂ -ᵥ y) +ᵥ 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]
-- 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₂ • (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
⊢ (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₉ : (y -ᵥ 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]
-- 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₂ • (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
⊢ (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
have h₁₀ : y = 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]
-- 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 y : P
hx : x ∈ s
hy : y ∉ s
⊢ s.SOppSide y ((pointReflection R x : (a : P) → P) y)
have refine : ∀ (h : x = y), y ∈ s
Tactic: refine (sbtw_pointReflection_of_ne R fun h => hy ?_).sOppSide_of_notMem_of_mem hy 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
h : (↑s : Set P).Nonempty
⊢ IsConnected.{u_4} (α := P) {y : P | s.WSameSide x y}
have obtain : ∀ (p : P) (hp : p ∈ (↑s : Set P)), IsConnected.{u_4} (α := P) {y : P | s.WSameSide 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.WSameSide x y}
have this : Nonempty.{u_4 + 1} ↥s
Tactic: haveI : Nonempty s := ⟨⟨p, hp⟩⟩