-- Mathlib/Analysis/Convex/Side.lean
theorem wOppSide_comm {s : AffineSubspace R P} {x y : P} : s.WOppSide x y ↔ s.WOppSide y x

Proof state:
case mp.intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : 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

Tactic:
refine ⟨p₂, hp₂, p₁, hp₁, ?_⟩

Result:
case mp.intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : 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)

Proof state:
case mp.intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : 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)

Tactic:
rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]

Result:
no goals

Proof state:
case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
⊢ s.WOppSide y x → s.WOppSide x y

Tactic:
rintro ⟨p₁, hp₁, p₂, hp₂, h⟩

Result:
case mpr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : 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

Proof state:
case mpr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : 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

Tactic:
refine ⟨p₂, hp₂, p₁, hp₁, ?_⟩

Result:
case mpr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : 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)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
⊢ s.WOppSide x y ↔ s.WOppSide y x

Tactic:
constructor

Result:
case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
⊢ s.WOppSide x y → s.WOppSide y x

case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
⊢ s.WOppSide y x → s.WOppSide x y

Proof state:
case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
⊢ s.WOppSide x y → s.WOppSide y x

Tactic:
rintro ⟨p₁, hp₁, p₂, hp₂, h⟩

Result:
case mp.intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : 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

Proof state:
case mpr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : 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)

Tactic:
rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]

Result:
no goals