awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ (AffineSubspace.map f s).WOppSide ((f : (a : P) → P') x) ((f : (a : P) → P') y)

Tactic:
⟨f p₁, mem_map_of_mem f hp₁, f p₂, mem_map_of_mem f hp₂, ?_⟩

Premises used: And.intro, Exists.intro, DFunLike.coe, AffineSubspace.mem_map_of_mem, AffineSubspace.WOppSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
refine :
  SameRay R (VSub.vsub.{u_3, u_5} (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') p₁ : P'))
    (VSub.vsub.{u_3, u_5} (P := P') ((f : (a : P) → P') p₂ : P') ((f : (a : P) → P') y : P'))
⊢ (AffineSubspace.map f s).WOppSide ((f : (a : P) → P') x) ((f : (a : P) → P') y)

Tactic:
refine ⟨f p₁, mem_map_of_mem f hp₁, f p₂, mem_map_of_mem f hp₂, ?_⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
simp_rw :
  SameRay.{u_1, u_3} R (M := V') ((f.linear : (a : V) → V') (x -ᵥ p₁) : V') ((f.linear : (a : V) → V') (p₂ -ᵥ y) : V')
⊢ SameRay R (VSub.vsub.{u_3, u_5} (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') p₁ : P'))
    (VSub.vsub.{u_3, u_5} (P := P') ((f : (a : P) → P') p₂ : P') ((f : (a : P) → P') y : P'))

Tactic:
simp_rw [← linearMap_vsub]

Premises used: AffineMap.linearMap_vsub
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ SameRay.{u_1, u_3} R (M := V') ((f.linear : (a : V) → V') (x -ᵥ p₁) : V') ((f.linear : (a : V) → V') (p₂ -ᵥ y) : V')

Tactic:
h.map f.linear

Premises used: SameRay.map, AffineMap.linear
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ SameRay.{u_1, u_3} R (M := V') ((f.linear : (a : V) → V') (x -ᵥ p₁) : V') ((f.linear : (a : V) → V') (p₂ -ᵥ y) : V')

Tactic:
exact h.map f.linear

Premises used: SameRay.map, AffineMap.linear
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
⊢ (map f s).WOppSide ((f : (a : P) → P') x) ((f : (a : P) → P') y) ↔ s.WOppSide x y

Tactic:
⟨fun h => ?_, fun h => h.map _⟩

Premises used: Iff.intro, AffineSubspace.WOppSide.map
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
refine : ∀ (h : (map f s).WOppSide ((f : (a : P) → P') x) ((f : (a : P) → P') y)), s.WOppSide x y
⊢ (map f s).WOppSide ((f : (a : P) → P') x) ((f : (a : P) → P') y) ↔ s.WOppSide x y

Tactic:
refine ⟨fun h => ?_, fun h => h.map _⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
h : (map f s).WOppSide ((f : (a : P) → P') x) ((f : (a : P) → P') y)
rcases :
  ∀ (fp₁ : P') (hfp₁ : fp₁ ∈ map f s) (fp₂ : P') (hfp₂ : fp₂ ∈ map f s)
    (h : SameRay R ((f : (a : P) → P') x -ᵥ fp₁) (fp₂ -ᵥ (f : (a : P) → P') y)), s.WOppSide x y
⊢ s.WOppSide x y

Tactic:
rcases h with ⟨fp₁, hfp₁, fp₂, hfp₂, h⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
fp₁ : P'
hfp₁ : fp₁ ∈ map f s
fp₂ : P'
hfp₂ : fp₂ ∈ map f s
h : SameRay R ((f : (a : P) → P') x -ᵥ fp₁) (fp₂ -ᵥ (f : (a : P) → P') y)
rw :
  ∀ (hfp₁ : ∃ y ∈ s, (f : (a : P) → P') y = fp₁) (fp₂ : P') (hfp₂ : ∃ y ∈ s, (f : (a : P) → P') y = fp₂)
    (h : SameRay R ((f : (a : P) → P') x -ᵥ fp₁) (fp₂ -ᵥ (f : (a : P) → P') y)), s.WOppSide x y
⊢ s.WOppSide x y

Tactic:
rw [mem_map] at hfp₁ hfp₂

Premises used: AffineSubspace.mem_map
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
fp₁ : P'
hfp₁ : ∃ y ∈ s, (f : (a : P) → P') y = fp₁
fp₂ : P'
hfp₂ : ∃ y ∈ s, (f : (a : P) → P') y = fp₂
h : SameRay R ((f : (a : P) → P') x -ᵥ fp₁) (fp₂ -ᵥ (f : (a : P) → P') y)
rcases :
  ∀ (p₁ : P) (hp₁ : p₁ ∈ s)
    (h :
      SameRay R (VSub.vsub.{u_3, u_5} (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') p₁ : P'))
        (fp₂ -ᵥ (f : (a : P) → P') y)),
    s.WOppSide x y
⊢ s.WOppSide x y

Tactic:
rcases hfp₁ with ⟨p₁, hp₁, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
fp₂ : P'
hfp₂ : ∃ y ∈ s, (f : (a : P) → P') y = fp₂
p₁ : P
hp₁ : p₁ ∈ s
h :
  SameRay R (VSub.vsub.{u_3, u_5} (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') p₁ : P'))
    (fp₂ -ᵥ (f : (a : P) → P') y)
rcases :
  ∀ (p₂ : P) (hp₂ : p₂ ∈ s)
    (h :
      SameRay R (VSub.vsub.{u_3, u_5} (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') p₁ : P'))
        (VSub.vsub.{u_3, u_5} (P := P') ((f : (a : P) → P') p₂ : P') ((f : (a : P) → P') y : P'))),
    s.WOppSide x y
⊢ s.WOppSide x y

Tactic:
rcases hfp₂ with ⟨p₂, hp₂, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h :
  SameRay R (VSub.vsub.{u_3, u_5} (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') p₁ : P'))
    (VSub.vsub.{u_3, u_5} (P := P') ((f : (a : P) → P') p₂ : P') ((f : (a : P) → P') y : P'))
⊢ s.WOppSide x y

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

Premises used: And.intro, Exists.intro, AffineSubspace.WOppSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h :
  SameRay R (VSub.vsub.{u_3, u_5} (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') p₁ : P'))
    (VSub.vsub.{u_3, u_5} (P := P') ((f : (a : P) → P') p₂ : P') ((f : (a : P) → P') y : P'))
refine : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ s.WOppSide x y

Tactic:
refine ⟨p₁, hp₁, p₂, hp₂, ?_⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h :
  SameRay R (VSub.vsub.{u_3, u_5} (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') p₁ : P'))
    (VSub.vsub.{u_3, u_5} (P := P') ((f : (a : P) → P') p₂ : P') ((f : (a : P) → P') y : P'))
⊢ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
simp_rw [← linearMap_vsub, (f.linear_injective_iff.2 hf).sameRay_map_iff] at h

Premises used: Iff.mpr, AffineMap.linear_injective_iff, AffineMap.linearMap_vsub, Function.Injective.sameRay_map_iff
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
h
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
exact h
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
simp_rw :
  (map f s).WOppSide ((f : (a : P) → P') x) ((f : (a : P) → P') y) ∧
      ((f : (a : P) → P') x : P') ∉ map f s ∧ ((f : (a : P) → P') y : P') ∉ map f s ↔
    s.WOppSide x y ∧ x ∉ s ∧ y ∉ s
simp_rw₁ :
  s.WOppSide x y ∧ ((f : (a : P) → P') x : P') ∉ map f s ∧ ((f : (a : P) → P') y : P') ∉ map f s ↔
    s.WOppSide x y ∧ x ∉ s ∧ y ∉ s
⊢ (map f s).SOppSide ((f : (a : P) → P') x) ((f : (a : P) → P') y) ↔ s.SOppSide x y

Tactic:
simp_rw [SOppSide, hf.wOppSide_map_iff, mem_map_iff_mem_of_injective hf]

Premises used: AffineSubspace.mem_map_iff_mem_of_injective, AffineSubspace.SOppSide, Function.Injective.wOppSide_map_iff
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P ≃ᵃ[R] P'
⊢ (map (↑f : P →ᵃ[R] P') s).WOppSide ((f : (a : P) → P') x) ((f : (a : P) → P') y) ↔ s.WOppSide x y

Tactic:
(show Function.Injective f.toAffineMap from f.injective).wOppSide_map_iff

Premises used: AffineEquiv.injective, Function.Injective.wOppSide_map_iff
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
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
inst_6 : AddCommGroup V'
inst_7 : Module R V'
inst_8 : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P ≃ᵃ[R] P'
⊢ (map (↑f : P →ᵃ[R] P') s).SOppSide ((f : (a : P) → P') x) ((f : (a : P) → P') y) ↔ s.SOppSide x y

Tactic:
(show Function.Injective f.toAffineMap from f.injective).sOppSide_map_iff

Premises used: Function.Injective.sOppSide_map_iff, AffineEquiv.injective
-- Module: Mathlib.Analysis.Convex.Side
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
h : s.WSameSide x y
⊢ (↑s : Set P).Nonempty

Tactic:
⟨h.choose, h.choose_spec.left⟩

Premises used: Exists.choose_spec, Set.Nonempty, And.left, Exists.intro, Exists.choose
-- Module: Mathlib.Analysis.Convex.Side
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
h : s.SSameSide x y
⊢ (↑s : Set P).Nonempty

Tactic:
⟨h.1.choose, h.1.choose_spec.left⟩

Premises used: Exists.choose_spec, Set.Nonempty, And.left, Exists.intro, Exists.choose
-- Module: Mathlib.Analysis.Convex.Side
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
h : s.WOppSide x y
⊢ (↑s : Set P).Nonempty

Tactic:
⟨h.choose, h.choose_spec.left⟩

Premises used: Exists.choose_spec, Set.Nonempty, And.left, Exists.intro, Exists.choose
-- Module: Mathlib.Analysis.Convex.Side
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
h : s.SOppSide x y
⊢ (↑s : Set P).Nonempty

Tactic:
⟨h.1.choose, h.1.choose_spec.left⟩

Premises used: Exists.choose_spec, Set.Nonempty, And.left, Exists.intro, Exists.choose
-- Module: Mathlib.Analysis.Convex.Side
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
h : s.SSameSide x y
⊢ s.WSameSide x y

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Analysis.Convex.Side
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
h : s.SSameSide x y
⊢ x ∉ s

Tactic:
h.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.Convex.Side
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
h : s.SSameSide x y
⊢ y ∉ s

Tactic:
h.2.2

Premises used: And.right
-- Module: Mathlib.Analysis.Convex.Side
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
h : s.SOppSide x y
⊢ s.WOppSide x y

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Analysis.Convex.Side
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
h : s.SOppSide x y
⊢ x ∉ s

Tactic:
h.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.Convex.Side
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
h : s.SOppSide x y
⊢ y ∉ s

Tactic:
h.2.2

Premises used: And.right
-- Module: Mathlib.Analysis.Convex.Side
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.WSameSide x y ↔ s.WSameSide y x

Tactic:
⟨fun ⟨p₁, hp₁, p₂, hp₂, h⟩ => ⟨p₂, hp₂, p₁, hp₁, h.symm⟩,
    fun ⟨p₁, hp₁, p₂, hp₂, h⟩ => ⟨p₂, hp₂, p₁, hp₁, h.symm⟩⟩

Premises used: _private.0.AffineSubspace.wSameSide_comm.match_1, SameRay.symm, _private.0.AffineSubspace.wSameSide_comm.match_2, And.intro, Iff.intro, Exists.intro, AffineSubspace.WSameSide
-- Module: Mathlib.Analysis.Convex.Side
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.WSameSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.SSameSide y x
rw₁ : s.WSameSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.WSameSide y x ∧ y ∉ s ∧ x ∉ s
rw₂ : s.WSameSide y x ∧ x ∉ s ∧ y ∉ s ↔ s.WSameSide y x ∧ y ∉ s ∧ x ∉ s
rw₃ rw₄ : s.WSameSide y x ∧ x ∉ s ∧ y ∉ s ↔ s.WSameSide y x ∧ x ∉ s ∧ y ∉ s
⊢ s.SSameSide x y ↔ s.SSameSide y x

Tactic:
rw [SSameSide, SSameSide, wSameSide_comm, and_comm (b := x ∉ s)]

Premises used: AffineSubspace.SSameSide, AffineSubspace.wSameSide_comm, and_comm
-- Module: Mathlib.Analysis.Convex.Side
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
mpr : s.WOppSide y x → s.WOppSide x y
⊢ s.WOppSide x y ↔ s.WOppSide y x

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Side
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

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

Premises used: And.intro, Exists.intro, AffineSubspace.WOppSide
-- Module: Mathlib.Analysis.Convex.Side
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 (y -ᵥ p₂) (p₁ -ᵥ x)
⊢ s.WOppSide y x

Tactic:
refine ⟨p₂, hp₂, p₁, hp₁, ?_⟩
-- Module: Mathlib.Analysis.Convex.Side
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₂))
mp₂ : SameRay R (x -ᵥ p₁) (-(y -ᵥ p₂))
mp₃ mp₄ mp₅ mp₆ : 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]

Premises used: SameRay.sameRay_comm, neg_vsub_eq_vsub_rev, sameRay_neg_iff
-- Module: Mathlib.Analysis.Convex.Side
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

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

Premises used: And.intro, Exists.intro, AffineSubspace.WOppSide
-- Module: Mathlib.Analysis.Convex.Side
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 (x -ᵥ p₂) (p₁ -ᵥ y)
⊢ s.WOppSide x y

Tactic:
refine ⟨p₂, hp₂, p₁, hp₁, ?_⟩
-- Module: Mathlib.Analysis.Convex.Side
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₂))
mpr₂ : SameRay R (y -ᵥ p₁) (-(x -ᵥ p₂))
mpr₃ mpr₄ mpr₅ mpr₆ : 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]

Premises used: SameRay.sameRay_comm, neg_vsub_eq_vsub_rev, sameRay_neg_iff
-- Module: Mathlib.Analysis.Convex.Side
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
rw₃ rw₄ : s.WOppSide y x ∧ x ∉ s ∧ y ∉ s ↔ s.WOppSide y x ∧ x ∉ s ∧ y ∉ s
⊢ s.SOppSide x y ↔ s.SOppSide y x

Tactic:
rw [SOppSide, SOppSide, wOppSide_comm, and_comm (b := x ∉ s)]

Premises used: AffineSubspace.wOppSide_comm, and_comm, AffineSubspace.SOppSide
-- Module: Mathlib.Analysis.Convex.Side
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
x y : P
⊢ ¬WSameSide.{u_1, u_2, u_4} (R := R) ⊥ x y

Tactic:
fun ⟨_, h, _⟩ => h.elim

Premises used: False, False.elim, _private.0.AffineSubspace.not_wSameSide_bot.match_1, Not