awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ update (β := M) y i '' [x₁ -[𝕜] x₂] = [update (β := M) y i x₁ -[𝕜] update (β := M) y i x₂]
have 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})
Tactic: rw [segment_eq_image₂, segment_eq_image₂, image_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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})
have 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₂
Tactic: refine EqOn.image_eq fun a ha ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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
⊢ update (β := M) y i '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (update (β := M) y i x₁) (update (β := M) y i x₂)
have 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})
Tactic: rw [openSegment_eq_image₂, openSegment_eq_image₂, image_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
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})
have 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₂
Tactic: refine EqOn.image_eq fun a ha ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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'
⊢ (AffineSubspace.map f s).WSameSide ((f : (a : P) → P') x) ((f : (a : P) → P') y)
have 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)
Tactic: rcases h with ⟨p₁, hp₁, p₂, hp₂, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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)
have 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'))
Tactic: refine ⟨f p₁, mem_map_of_mem f hp₁, f p₂, mem_map_of_mem f hp₂, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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 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'))
have 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')
Tactic: simp_rw [← linearMap_vsub]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
have refine : ∀ (h : (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 _⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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)
⊢ s.WSameSide x y
have 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
Tactic: rcases h with ⟨fp₁, hfp₁, fp₂, hfp₂, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₂)
⊢ s.WSameSide x y
have 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
Tactic: rw [mem_map] at hfp₁ hfp₂
Cleared hypotheses: hfp₁, fp₂, hfp₂, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₂)
⊢ s.WSameSide x y
have 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
Tactic: rcases hfp₁ with ⟨p₁, hp₁, rfl⟩
Cleared hypotheses: fp₁, hfp₁, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₂)
⊢ s.WSameSide x y
have 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
Tactic: rcases hfp₂ with ⟨p₂, hp₂, rfl⟩
Cleared hypotheses: fp₂, hfp₂, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
have refine : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
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
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).SSameSide ((f : (a : P) → P') x) ((f : (a : P) → P') y) ↔ s.SSameSide x y
have 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
Tactic: simp_rw [SSameSide, hf.wSameSide_map_iff, mem_map_iff_mem_of_injective hf]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ (map f s).SSameSide ((f : (a : P) → P') x) ((f : (a : P) → P') y) ↔ s.SSameSide x y
have 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
Tactic: simp_rw [SSameSide, hf.wSameSide_map_iff, mem_map_iff_mem_of_injective hf]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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'
⊢ (AffineSubspace.map f s).WOppSide ((f : (a : P) → P') x) ((f : (a : P) → P') y)
have 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)
Tactic: rcases h with ⟨p₁, hp₁, p₂, hp₂, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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)
have 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'))
Tactic: refine ⟨f p₁, mem_map_of_mem f hp₁, f p₂, mem_map_of_mem f hp₂, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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 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'))
have 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')
Tactic: simp_rw [← linearMap_vsub]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
have refine : ∀ (h : (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 _⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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)
⊢ s.WOppSide x y
have 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
Tactic: rcases h with ⟨fp₁, hfp₁, fp₂, hfp₂, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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)
⊢ s.WOppSide x y
have 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
Tactic: rw [mem_map] at hfp₁ hfp₂
Cleared hypotheses: hfp₁, fp₂, hfp₂, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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)
⊢ s.WOppSide x y
have 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
Tactic: rcases hfp₁ with ⟨p₁, hp₁, rfl⟩
Cleared hypotheses: fp₁, hfp₁, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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)
⊢ s.WOppSide x y
have 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
Tactic: rcases hfp₂ with ⟨p₂, hp₂, rfl⟩
Cleared hypotheses: fp₂, hfp₂, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
have refine : 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
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).SOppSide ((f : (a : P) → P') x) ((f : (a : P) → P') y) ↔ s.SOppSide x y
have 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
Tactic: simp_rw [SOppSide, hf.wOppSide_map_iff, mem_map_iff_mem_of_injective hf]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ (map f s).SOppSide ((f : (a : P) → P') x) ((f : (a : P) → P') y) ↔ s.SOppSide x y
have 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
Tactic: simp_rw [SOppSide, hf.wOppSide_map_iff, mem_map_iff_mem_of_injective hf]
-- 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.SSameSide x y ↔ s.SSameSide y x
have rw : s.WSameSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.SSameSide y x
Tactic: rw [SSameSide, SSameSide, wSameSide_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.WSameSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.SSameSide y x
⊢ s.SSameSide x y ↔ s.SSameSide y x
have rw₁ : s.WSameSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.WSameSide y x ∧ y ∉ s ∧ x ∉ s
Tactic: rw [SSameSide, SSameSide, wSameSide_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.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
⊢ s.SSameSide x y ↔ s.SSameSide y x
have rw₂ : s.WSameSide y x ∧ x ∉ s ∧ y ∉ s ↔ s.WSameSide y x ∧ y ∉ s ∧ x ∉ s
Tactic: rw [SSameSide, SSameSide, wSameSide_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.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
⊢ s.SSameSide x y ↔ s.SSameSide y x
have rw₃ : s.WSameSide y x ∧ x ∉ s ∧ y ∉ s ↔ s.WSameSide y x ∧ x ∉ s ∧ y ∉ s
Tactic: rw [SSameSide, SSameSide, wSameSide_comm, and_comm (b := x ∉ s)]