awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_6} 𝕜 (M i)
s : Set ι
x y z : (i : ι) → M i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a • x + b • y = z
i : ι
⊢ Membership.mem (γ := Set (M i)) ((fun (i : ι) ↦ [x i -[𝕜] y i]) i) (z i)

Tactic:
⟨a, b, ha, hb, hab, congr_fun hz i⟩

Premises used: Set.Mem, setOf, segment, And.intro, Exists.intro, congr_fun
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_6} 𝕜 (M i)
s : Set ι
x y z : (i : ι) → M i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a • x + b • y = z
i : ι
⊢ Membership.mem (γ := Set (M i)) ((fun (i : ι) ↦ [x i -[𝕜] y i]) i) (z i)

Tactic:
exact ⟨a, b, ha, hb, hab, congr_fun hz i⟩
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_6} 𝕜 (M i)
s : Set ι
x y z : (i : ι) → M i
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = z
i : ι
⊢ Membership.mem (γ := Set (M i)) ((fun (i : ι) ↦ openSegment 𝕜 (x i) (y i)) i) (z i)

Tactic:
⟨a, b, ha, hb, hab, congr_fun hz i⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, openSegment, congr_fun
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_6} 𝕜 (M i)
s : Set ι
x y z : (i : ι) → M i
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = z
i : ι
⊢ Membership.mem (γ := Set (M i)) ((fun (i : ι) ↦ openSegment 𝕜 (x i) (y i)) i) (z i)

Tactic:
exact ⟨a, b, ha, hb, hab, congr_fun hz i⟩
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_6} 𝕜 (M i)
inst_4 : DecidableEq ι
i : ι
x₁ x₂ : M i
y : (i : ι) → M i
rw :
  Eq (α := Set ((a : ι) → M a))
    ((fun (x : 𝕜 × 𝕜) ↦ update (β := M) y i (x.1 • x₁ + x.2 • x₂)) '' {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1})
    ((fun (p : 𝕜 × 𝕜) ↦ p.1 • update (β := M) y i x₁ + p.2 • update (β := M) y i x₂) ''
      {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1})
⊢ update (β := M) y i '' [x₁ -[𝕜] x₂] = [update (β := M) y i x₁ -[𝕜] update (β := M) y i x₂]

Tactic:
rw [segment_eq_image₂, segment_eq_image₂, image_image]

Premises used: Set.image_image, segment_eq_image₂
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_6} 𝕜 (M i)
inst_4 : DecidableEq ι
i : ι
x₁ x₂ : M i
y : (i : ι) → M i
⊢ Eq (α := Set ((a : ι) → M a))
    ((fun (x : 𝕜 × 𝕜) ↦ update (β := M) y i (x.1 • x₁ + x.2 • x₂)) '' {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1})
    ((fun (p : 𝕜 × 𝕜) ↦ p.1 • update (β := M) y i x₁ + p.2 • update (β := M) y i x₂) ''
      {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1})

Tactic:
EqOn.image_eq fun a ha ↦ ?_

Premises used: Set.EqOn.image_eq
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_6} 𝕜 (M i)
inst_4 : DecidableEq ι
i : ι
x₁ x₂ : M i
y : (i : ι) → M i
refine :
  ∀ (a : 𝕜 × 𝕜) (ha : Membership.mem (γ := Set (𝕜 × 𝕜)) {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} a),
    update (β := M) y i (a.1 • x₁ + a.2 • x₂) = a.1 • update (β := M) y i x₁ + a.2 • update (β := M) y i x₂
⊢ Eq (α := Set ((a : ι) → M a))
    ((fun (x : 𝕜 × 𝕜) ↦ update (β := M) y i (x.1 • x₁ + x.2 • x₂)) '' {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1})
    ((fun (p : 𝕜 × 𝕜) ↦ p.1 • update (β := M) y i x₁ + p.2 • update (β := M) y i x₂) ''
      {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1})

Tactic:
refine EqOn.image_eq fun a ha ↦ ?_

Premises used: Set.EqOn.image_eq
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_6} 𝕜 (M i)
inst_4 : DecidableEq ι
i : ι
x₁ x₂ : M i
y : (i : ι) → M i
a : 𝕜 × 𝕜
ha : Membership.mem (γ := Set (𝕜 × 𝕜)) {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} a
⊢ update (β := M) y i (a.1 • x₁ + a.2 • x₂) = a.1 • update (β := M) y i x₁ + a.2 • update (β := M) y i x₂

Tactic:
simp only [← update_smul, ← update_add, Convex.combo_self ha.2.2]

Premises used: Function.update_smul, Convex.combo_self, And.right, Function.update_add
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_6} 𝕜 (M i)
inst_4 : DecidableEq ι
i : ι
x₁ x₂ : M i
y : (i : ι) → M i
rw :
  Eq (α := Set ((a : ι) → M a))
    ((fun (x : 𝕜 × 𝕜) ↦ update (β := M) y i (x.1 • x₁ + x.2 • x₂)) '' {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1})
    ((fun (p : 𝕜 × 𝕜) ↦ p.1 • update (β := M) y i x₁ + p.2 • update (β := M) y i x₂) ''
      {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1})
⊢ update (β := M) y i '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (update (β := M) y i x₁) (update (β := M) y i x₂)

Tactic:
rw [openSegment_eq_image₂, openSegment_eq_image₂, image_image]

Premises used: Set.image_image, openSegment_eq_image₂
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_6} 𝕜 (M i)
inst_4 : DecidableEq ι
i : ι
x₁ x₂ : M i
y : (i : ι) → M i
⊢ Eq (α := Set ((a : ι) → M a))
    ((fun (x : 𝕜 × 𝕜) ↦ update (β := M) y i (x.1 • x₁ + x.2 • x₂)) '' {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1})
    ((fun (p : 𝕜 × 𝕜) ↦ p.1 • update (β := M) y i x₁ + p.2 • update (β := M) y i x₂) ''
      {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1})

Tactic:
EqOn.image_eq fun a ha ↦ ?_

Premises used: Set.EqOn.image_eq
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_6} 𝕜 (M i)
inst_4 : DecidableEq ι
i : ι
x₁ x₂ : M i
y : (i : ι) → M i
refine :
  ∀ (a : 𝕜 × 𝕜) (ha : Membership.mem (γ := Set (𝕜 × 𝕜)) {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} a),
    update (β := M) y i (a.1 • x₁ + a.2 • x₂) = a.1 • update (β := M) y i x₁ + a.2 • update (β := M) y i x₂
⊢ Eq (α := Set ((a : ι) → M a))
    ((fun (x : 𝕜 × 𝕜) ↦ update (β := M) y i (x.1 • x₁ + x.2 • x₂)) '' {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1})
    ((fun (p : 𝕜 × 𝕜) ↦ p.1 • update (β := M) y i x₁ + p.2 • update (β := M) y i x₂) ''
      {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1})

Tactic:
refine EqOn.image_eq fun a ha ↦ ?_

Premises used: Set.EqOn.image_eq
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_6} 𝕜 (M i)
inst_4 : DecidableEq ι
i : ι
x₁ x₂ : M i
y : (i : ι) → M i
a : 𝕜 × 𝕜
ha : Membership.mem (γ := Set (𝕜 × 𝕜)) {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} a
⊢ update (β := M) y i (a.1 • x₁ + a.2 • x₂) = a.1 • update (β := M) y i x₁ + a.2 • update (β := M) y i x₂

Tactic:
simp only [← update_smul, ← update_add, Convex.combo_self ha.2.2]

Premises used: Function.update_smul, Convex.combo_self, And.right, Function.update_add
-- 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
h : s.WSameSide x y
f : P →ᵃ[R] P'
rcases :
  ∀ (p₁ : P) (hp₁ : p₁ ∈ s) (p₂ : P) (hp₂ : p₂ ∈ s) (h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)),
    (AffineSubspace.map f s).WSameSide ((f : (a : P) → P') x) ((f : (a : P) → P') y)
⊢ (AffineSubspace.map f s).WSameSide ((f : (a : P) → P') x) ((f : (a : P) → P') y)

Tactic:
rcases h with ⟨p₁, hp₁, p₂, hp₂, 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'
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ (AffineSubspace.map f s).WSameSide ((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.WSameSide, AffineSubspace.mem_map_of_mem
-- 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₁) (y -ᵥ p₂)
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') y : P') ((f : (a : P) → P') p₂ : P'))
⊢ (AffineSubspace.map f s).WSameSide ((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₁) (y -ᵥ p₂)
simp_rw :
  SameRay.{u_1, u_3} R (M := V') ((f.linear : (a : V) → V') (x -ᵥ p₁) : V') ((f.linear : (a : V) → V') (y -ᵥ p₂) : 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') y : P') ((f : (a : P) → P') p₂ : 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₁) (y -ᵥ p₂)
⊢ SameRay.{u_1, u_3} R (M := V') ((f.linear : (a : V) → V') (x -ᵥ p₁) : V') ((f.linear : (a : V) → V') (y -ᵥ p₂) : 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₁) (y -ᵥ p₂)
⊢ SameRay.{u_1, u_3} R (M := V') ((f.linear : (a : V) → V') (x -ᵥ p₁) : V') ((f.linear : (a : V) → V') (y -ᵥ p₂) : 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).WSameSide ((f : (a : P) → P') x) ((f : (a : P) → P') y) ↔ s.WSameSide x y

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

Premises used: AffineSubspace.WSameSide.map, Iff.intro
-- 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).WSameSide ((f : (a : P) → P') x) ((f : (a : P) → P') y)), s.WSameSide x y
⊢ (map f s).WSameSide ((f : (a : P) → P') x) ((f : (a : P) → P') y) ↔ s.WSameSide 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).WSameSide ((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₁) ((f : (a : P) → P') y -ᵥ fp₂)), s.WSameSide x y
⊢ s.WSameSide 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₁) ((f : (a : P) → P') y -ᵥ fp₂)
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₁) ((f : (a : P) → P') y -ᵥ fp₂)), s.WSameSide x y
⊢ s.WSameSide 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₁) ((f : (a : P) → P') y -ᵥ fp₂)
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'))
        ((f : (a : P) → P') y -ᵥ fp₂)),
    s.WSameSide x y
⊢ s.WSameSide 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'))
    ((f : (a : P) → P') y -ᵥ fp₂)
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') y : P') ((f : (a : P) → P') p₂ : P'))),
    s.WSameSide x y
⊢ s.WSameSide 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') y : P') ((f : (a : P) → P') p₂ : P'))
⊢ s.WSameSide x y

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

Premises used: And.intro, Exists.intro, AffineSubspace.WSameSide
-- 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') y : P') ((f : (a : P) → P') p₂ : P'))
refine : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
⊢ s.WSameSide 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') y : P') ((f : (a : P) → P') p₂ : P'))
⊢ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

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₁) (y -ᵥ p₂)
⊢ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

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₁) (y -ᵥ p₂)
⊢ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

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).WSameSide ((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.WSameSide x y ∧ x ∉ s ∧ y ∉ s
simp_rw₁ :
  s.WSameSide x y ∧ ((f : (a : P) → P') x : P') ∉ map f s ∧ ((f : (a : P) → P') y : P') ∉ map f s ↔
    s.WSameSide x y ∧ x ∉ s ∧ y ∉ s
⊢ (map f s).SSameSide ((f : (a : P) → P') x) ((f : (a : P) → P') y) ↔ s.SSameSide x y

Tactic:
simp_rw [SSameSide, hf.wSameSide_map_iff, mem_map_iff_mem_of_injective hf]

Premises used: AffineSubspace.SSameSide, AffineSubspace.mem_map_iff_mem_of_injective, Function.Injective.wSameSide_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).WSameSide ((f : (a : P) → P') x) ((f : (a : P) → P') y) ↔ s.WSameSide x y

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

Premises used: AffineEquiv.injective, Function.Injective.wSameSide_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).SSameSide ((f : (a : P) → P') x) ((f : (a : P) → P') y) ↔ s.SSameSide x y

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

Premises used: Function.Injective.sSameSide_map_iff, AffineEquiv.injective
-- 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
h : s.WOppSide x y
f : P →ᵃ[R] P'
rcases :
  ∀ (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)
⊢ (AffineSubspace.map f s).WOppSide ((f : (a : P) → P') x) ((f : (a : P) → P') y)

Tactic:
rcases h with ⟨p₁, hp₁, p₂, hp₂, h⟩