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 : CommRing R
inst_1 : PartialOrder 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
⊢ s.WOppSide x y ↔ s.WOppSide y x
have mp : s.WOppSide x y → s.WOppSide y x
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 : CommRing R
inst_1 : PartialOrder 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
mp : s.WOppSide x y → s.WOppSide y x
⊢ s.WOppSide x y ↔ s.WOppSide y x
have mpr : s.WOppSide y x → s.WOppSide 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 : CommRing R
inst_1 : PartialOrder 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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ s.WOppSide y x
have mp : SameRay R (y -ᵥ p₂) (p₁ -ᵥ x)
Tactic: refine ⟨p₂, hp₂, 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 : CommRing R
inst_1 : PartialOrder 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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ SameRay R (y -ᵥ p₂) (p₁ -ᵥ x)
have mp : SameRay R (p₁ -ᵥ x) (y -ᵥ p₂)
Tactic: rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
mp : SameRay R (p₁ -ᵥ x) (y -ᵥ p₂)
⊢ SameRay R (y -ᵥ p₂) (p₁ -ᵥ x)
have mp₁ : SameRay R (-(p₁ -ᵥ x)) (-(y -ᵥ p₂))
Tactic: rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
mp : SameRay R (p₁ -ᵥ x) (y -ᵥ p₂)
mp₁ : SameRay R (-(p₁ -ᵥ x)) (-(y -ᵥ p₂))
⊢ SameRay R (y -ᵥ p₂) (p₁ -ᵥ x)
have mp₂ : SameRay R (x -ᵥ p₁) (-(y -ᵥ p₂))
Tactic: rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (y -ᵥ p₁) (p₂ -ᵥ x)
⊢ s.WOppSide x y
have mpr : SameRay R (x -ᵥ p₂) (p₁ -ᵥ y)
Tactic: refine ⟨p₂, hp₂, 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 : CommRing R
inst_1 : PartialOrder 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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (y -ᵥ p₁) (p₂ -ᵥ x)
⊢ SameRay R (x -ᵥ p₂) (p₁ -ᵥ y)
have mpr : SameRay R (p₁ -ᵥ y) (x -ᵥ p₂)
Tactic: rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (y -ᵥ p₁) (p₂ -ᵥ x)
mpr : SameRay R (p₁ -ᵥ y) (x -ᵥ p₂)
⊢ SameRay R (x -ᵥ p₂) (p₁ -ᵥ y)
have mpr₁ : SameRay R (-(p₁ -ᵥ y)) (-(x -ᵥ p₂))
Tactic: rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (y -ᵥ p₁) (p₂ -ᵥ x)
mpr : SameRay R (p₁ -ᵥ y) (x -ᵥ p₂)
mpr₁ : SameRay R (-(p₁ -ᵥ y)) (-(x -ᵥ p₂))
⊢ SameRay R (x -ᵥ p₂) (p₁ -ᵥ y)
have mpr₂ : SameRay R (y -ᵥ p₁) (-(x -ᵥ p₂))
Tactic: rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
⊢ s.SOppSide x y ↔ s.SOppSide y x
have rw : s.WOppSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.SOppSide y x
Tactic: rw [SOppSide, SOppSide, wOppSide_comm, and_comm (b := x ∉ s)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
rw : s.WOppSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.SOppSide y x
⊢ s.SOppSide x y ↔ s.SOppSide y x
have rw₁ : s.WOppSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.WOppSide y x ∧ y ∉ s ∧ x ∉ s
Tactic: rw [SOppSide, SOppSide, wOppSide_comm, and_comm (b := x ∉ s)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
rw : s.WOppSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.SOppSide y x
rw₁ : s.WOppSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.WOppSide y x ∧ y ∉ s ∧ x ∉ s
⊢ s.SOppSide x y ↔ s.SOppSide y x
have rw₂ : s.WOppSide y x ∧ x ∉ s ∧ y ∉ s ↔ s.WOppSide y x ∧ y ∉ s ∧ x ∉ s
Tactic: rw [SOppSide, SOppSide, wOppSide_comm, and_comm (b := x ∉ s)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
rw : s.WOppSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.SOppSide y x
rw₁ : s.WOppSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.WOppSide y x ∧ y ∉ s ∧ x ∉ s
rw₂ : s.WOppSide y x ∧ x ∉ s ∧ y ∉ s ↔ s.WOppSide y x ∧ y ∉ s ∧ x ∉ s
⊢ s.SOppSide x y ↔ s.SOppSide y x
have rw₃ : s.WOppSide y x ∧ x ∉ s ∧ y ∉ s ↔ s.WOppSide y x ∧ x ∉ s ∧ y ∉ s
Tactic: rw [SOppSide, SOppSide, wOppSide_comm, and_comm (b := x ∉ s)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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.WSameSide x y
have refine : SameRay R (x -ᵥ x) (y -ᵥ x)
Tactic: refine ⟨x, hx, x, 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 : CommRing R
inst_1 : PartialOrder 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
⊢ SameRay R (x -ᵥ x) (y -ᵥ x)
have rw : SameRay R 0 (y -ᵥ x)
Tactic: rw [vsub_self]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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 x y
have refine : SameRay R (x -ᵥ x) (x -ᵥ y)
Tactic: refine ⟨x, hx, x, 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 : CommRing R
inst_1 : PartialOrder 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
⊢ SameRay R (x -ᵥ x) (x -ᵥ y)
have rw : SameRay R 0 (x -ᵥ y)
Tactic: rw [vsub_self]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
⊢ s.WSameSide (v +ᵥ x) y ↔ s.WSameSide x y
have mp : s.WSameSide (v +ᵥ x) 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 : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
mp : s.WSameSide (v +ᵥ x) y → s.WSameSide x y
⊢ s.WSameSide (v +ᵥ x) y ↔ s.WSameSide x y
have mpr : s.WSameSide x y → s.WSameSide (v +ᵥ 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 : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (y -ᵥ p₂)
⊢ s.WSameSide x y
have mp : SameRay R (x -ᵥ (-v +ᵥ p₁)) (y -ᵥ p₂)
Tactic: refine
      ⟨-v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) hp₁, 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 : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (y -ᵥ p₂)
⊢ SameRay R (x -ᵥ (-v +ᵥ p₁)) (y -ᵥ p₂)
have mp : SameRay R (x -ᵥ p₁ - -v) (y -ᵥ p₂)
Tactic: rwa [vsub_vadd_eq_vsub_sub, sub_neg_eq_add, add_comm, ← vadd_vsub_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (y -ᵥ p₂)
mp : SameRay R (x -ᵥ p₁ - -v) (y -ᵥ p₂)
⊢ SameRay R (x -ᵥ (-v +ᵥ p₁)) (y -ᵥ p₂)
have mp₁ : SameRay R (x -ᵥ p₁ + v) (y -ᵥ p₂)
Tactic: rwa [vsub_vadd_eq_vsub_sub, sub_neg_eq_add, add_comm, ← vadd_vsub_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (y -ᵥ p₂)
mp : SameRay R (x -ᵥ p₁ - -v) (y -ᵥ p₂)
mp₁ : SameRay R (x -ᵥ p₁ + v) (y -ᵥ p₂)
⊢ SameRay R (x -ᵥ (-v +ᵥ p₁)) (y -ᵥ p₂)
have mp₂ : SameRay R (v + (x -ᵥ p₁)) (y -ᵥ p₂)
Tactic: rwa [vsub_vadd_eq_vsub_sub, sub_neg_eq_add, add_comm, ← vadd_vsub_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ s.WSameSide (v +ᵥ x) y
have mpr : SameRay R ((v +ᵥ x) -ᵥ (v +ᵥ p₁)) (y -ᵥ p₂)
Tactic: refine ⟨v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction hv hp₁, 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 : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
⊢ s.WSameSide x (v +ᵥ y) ↔ s.WSameSide x y
have rw : s.WSameSide (v +ᵥ y) x ↔ s.WSameSide x y
Tactic: rw [wSameSide_comm, wSameSide_vadd_left_iff hv, wSameSide_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
rw : s.WSameSide (v +ᵥ y) x ↔ s.WSameSide x y
⊢ s.WSameSide x (v +ᵥ y) ↔ s.WSameSide x y
have rw₁ : s.WSameSide y x ↔ s.WSameSide x y
Tactic: rw [wSameSide_comm, wSameSide_vadd_left_iff hv, wSameSide_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
rw : s.WSameSide (v +ᵥ y) x ↔ s.WSameSide x y
rw₁ : s.WSameSide y x ↔ s.WSameSide x y
⊢ s.WSameSide x (v +ᵥ y) ↔ s.WSameSide x y
have rw₂ : s.WSameSide x y ↔ s.WSameSide x y
Tactic: rw [wSameSide_comm, wSameSide_vadd_left_iff hv, wSameSide_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
⊢ s.SSameSide (v +ᵥ x) y ↔ s.SSameSide x y
have rw : s.WSameSide (v +ᵥ x) y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.SSameSide x y
Tactic: rw [SSameSide, SSameSide, wSameSide_vadd_left_iff hv, vadd_mem_iff_mem_of_mem_direction hv]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
rw : s.WSameSide (v +ᵥ x) y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.SSameSide x y
⊢ s.SSameSide (v +ᵥ x) y ↔ s.SSameSide x y
have rw₁ : s.WSameSide (v +ᵥ x) y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.WSameSide x y ∧ x ∉ s ∧ y ∉ s
Tactic: rw [SSameSide, SSameSide, wSameSide_vadd_left_iff hv, vadd_mem_iff_mem_of_mem_direction hv]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
rw : s.WSameSide (v +ᵥ x) y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.SSameSide x y
rw₁ : s.WSameSide (v +ᵥ x) y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.WSameSide x y ∧ x ∉ s ∧ y ∉ s
⊢ s.SSameSide (v +ᵥ x) y ↔ s.SSameSide x y
have rw₂ : s.WSameSide x y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.WSameSide x y ∧ x ∉ s ∧ y ∉ s
Tactic: rw [SSameSide, SSameSide, wSameSide_vadd_left_iff hv, vadd_mem_iff_mem_of_mem_direction hv]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
rw : s.WSameSide (v +ᵥ x) y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.SSameSide x y
rw₁ : s.WSameSide (v +ᵥ x) y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.WSameSide x y ∧ x ∉ s ∧ y ∉ s
rw₂ : s.WSameSide x y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.WSameSide x y ∧ x ∉ s ∧ y ∉ s
⊢ s.SSameSide (v +ᵥ x) y ↔ s.SSameSide x y
have rw₃ : s.WSameSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.WSameSide x y ∧ x ∉ s ∧ y ∉ s
Tactic: rw [SSameSide, SSameSide, wSameSide_vadd_left_iff hv, vadd_mem_iff_mem_of_mem_direction hv]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
⊢ s.SSameSide x (v +ᵥ y) ↔ s.SSameSide x y
have rw : s.SSameSide (v +ᵥ y) x ↔ s.SSameSide x y
Tactic: rw [sSameSide_comm, sSameSide_vadd_left_iff hv, sSameSide_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
rw : s.SSameSide (v +ᵥ y) x ↔ s.SSameSide x y
⊢ s.SSameSide x (v +ᵥ y) ↔ s.SSameSide x y
have rw₁ : s.SSameSide y x ↔ s.SSameSide x y
Tactic: rw [sSameSide_comm, sSameSide_vadd_left_iff hv, sSameSide_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
rw : s.SSameSide (v +ᵥ y) x ↔ s.SSameSide x y
rw₁ : s.SSameSide y x ↔ s.SSameSide x y
⊢ s.SSameSide x (v +ᵥ y) ↔ s.SSameSide x y
have rw₂ : s.SSameSide x y ↔ s.SSameSide x y
Tactic: rw [sSameSide_comm, sSameSide_vadd_left_iff hv, sSameSide_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
⊢ s.WOppSide (v +ᵥ x) y ↔ s.WOppSide x y
have mp : s.WOppSide (v +ᵥ x) y → s.WOppSide 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 : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
mp : s.WOppSide (v +ᵥ x) y → s.WOppSide x y
⊢ s.WOppSide (v +ᵥ x) y ↔ s.WOppSide x y
have mpr : s.WOppSide x y → s.WOppSide (v +ᵥ 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 : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (p₂ -ᵥ y)
⊢ s.WOppSide x y
have mp : SameRay R (x -ᵥ (-v +ᵥ p₁)) (p₂ -ᵥ y)
Tactic: refine
      ⟨-v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) hp₁, 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 : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (p₂ -ᵥ y)
⊢ SameRay R (x -ᵥ (-v +ᵥ p₁)) (p₂ -ᵥ y)
have mp : SameRay R (x -ᵥ p₁ - -v) (p₂ -ᵥ y)
Tactic: rwa [vsub_vadd_eq_vsub_sub, sub_neg_eq_add, add_comm, ← vadd_vsub_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (p₂ -ᵥ y)
mp : SameRay R (x -ᵥ p₁ - -v) (p₂ -ᵥ y)
⊢ SameRay R (x -ᵥ (-v +ᵥ p₁)) (p₂ -ᵥ y)
have mp₁ : SameRay R (x -ᵥ p₁ + v) (p₂ -ᵥ y)
Tactic: rwa [vsub_vadd_eq_vsub_sub, sub_neg_eq_add, add_comm, ← vadd_vsub_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (p₂ -ᵥ y)
mp : SameRay R (x -ᵥ p₁ - -v) (p₂ -ᵥ y)
mp₁ : SameRay R (x -ᵥ p₁ + v) (p₂ -ᵥ y)
⊢ SameRay R (x -ᵥ (-v +ᵥ p₁)) (p₂ -ᵥ y)
have mp₂ : SameRay R (v + (x -ᵥ p₁)) (p₂ -ᵥ y)
Tactic: rwa [vsub_vadd_eq_vsub_sub, sub_neg_eq_add, add_comm, ← vadd_vsub_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ s.WOppSide (v +ᵥ x) y
have mpr : SameRay R ((v +ᵥ x) -ᵥ (v +ᵥ p₁)) (p₂ -ᵥ y)
Tactic: refine ⟨v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction hv hp₁, 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 : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
⊢ s.WOppSide x (v +ᵥ y) ↔ s.WOppSide x y
have rw : s.WOppSide (v +ᵥ y) x ↔ s.WOppSide x y
Tactic: rw [wOppSide_comm, wOppSide_vadd_left_iff hv, wOppSide_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
rw : s.WOppSide (v +ᵥ y) x ↔ s.WOppSide x y
⊢ s.WOppSide x (v +ᵥ y) ↔ s.WOppSide x y
have rw₁ : s.WOppSide y x ↔ s.WOppSide x y
Tactic: rw [wOppSide_comm, wOppSide_vadd_left_iff hv, wOppSide_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
rw : s.WOppSide (v +ᵥ y) x ↔ s.WOppSide x y
rw₁ : s.WOppSide y x ↔ s.WOppSide x y
⊢ s.WOppSide x (v +ᵥ y) ↔ s.WOppSide x y
have rw₂ : s.WOppSide x y ↔ s.WOppSide x y
Tactic: rw [wOppSide_comm, wOppSide_vadd_left_iff hv, wOppSide_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : CommRing R
inst_1 : PartialOrder 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
v : V
hv : v ∈ s.direction
⊢ s.SOppSide (v +ᵥ x) y ↔ s.SOppSide x y
have rw : s.WOppSide (v +ᵥ x) y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.SOppSide x y
Tactic: rw [SOppSide, SOppSide, wOppSide_vadd_left_iff hv, vadd_mem_iff_mem_of_mem_direction hv]