awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z : P
v : V
⊢ v +ᵥ z ∈ affineSegment R (v +ᵥ x) (v +ᵥ y) ↔ z ∈ affineSegment R x y
have rw : Membership.mem (γ := Set P) ((fun (x : P) ↦ v +ᵥ x) '' affineSegment R x y) (v +ᵥ z) ↔ z ∈ affineSegment R x y
Tactic: rw [← affineSegment_const_vadd_image, (AddAction.injective v).mem_set_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z : P
v : V
rw : Membership.mem (γ := Set P) ((fun (x : P) ↦ v +ᵥ x) '' affineSegment R x y) (v +ᵥ z) ↔ z ∈ affineSegment R x y
⊢ v +ᵥ z ∈ affineSegment R (v +ᵥ x) (v +ᵥ y) ↔ z ∈ affineSegment R x y
have rw₁ : z ∈ affineSegment R x y ↔ z ∈ affineSegment R x y
Tactic: rw [← affineSegment_const_vadd_image, (AddAction.injective v).mem_set_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z : V
p : P
⊢ z +ᵥ p ∈ affineSegment R (x +ᵥ p) (y +ᵥ p) ↔ z ∈ affineSegment R x y
have rw : Membership.mem (γ := Set P) ((fun (x : V) ↦ x +ᵥ p) '' affineSegment R x y) (z +ᵥ p) ↔ z ∈ affineSegment R x y
Tactic: rw [← affineSegment_vadd_const_image, (vadd_right_injective p).mem_set_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z : V
p : P
rw : Membership.mem (γ := Set P) ((fun (x : V) ↦ x +ᵥ p) '' affineSegment R x y) (z +ᵥ p) ↔ z ∈ affineSegment R x y
⊢ z +ᵥ p ∈ affineSegment R (x +ᵥ p) (y +ᵥ p) ↔ z ∈ affineSegment R x y
have rw₁ : z ∈ affineSegment R x y ↔ z ∈ affineSegment R x y
Tactic: rw [← affineSegment_vadd_const_image, (vadd_right_injective p).mem_set_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z p : P
⊢ p -ᵥ z ∈ affineSegment R (p -ᵥ x) (p -ᵥ y) ↔ z ∈ affineSegment R x y
have rw : Membership.mem (γ := Set V) ((fun (x : P) ↦ p -ᵥ x) '' affineSegment R x y) (p -ᵥ z) ↔ z ∈ affineSegment R x y
Tactic: rw [← affineSegment_const_vsub_image, (vsub_right_injective p).mem_set_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z p : P
rw : Membership.mem (γ := Set V) ((fun (x : P) ↦ p -ᵥ x) '' affineSegment R x y) (p -ᵥ z) ↔ z ∈ affineSegment R x y
⊢ p -ᵥ z ∈ affineSegment R (p -ᵥ x) (p -ᵥ y) ↔ z ∈ affineSegment R x y
have rw₁ : z ∈ affineSegment R x y ↔ z ∈ affineSegment R x y
Tactic: rw [← affineSegment_const_vsub_image, (vsub_right_injective p).mem_set_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z p : P
⊢ z -ᵥ p ∈ affineSegment R (x -ᵥ p) (y -ᵥ p) ↔ z ∈ affineSegment R x y
have rw : Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ p) '' affineSegment R x y) (z -ᵥ p) ↔ z ∈ affineSegment R x y
Tactic: rw [← affineSegment_vsub_const_image, (vsub_left_injective p).mem_set_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z p : P
rw : Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ p) '' affineSegment R x y) (z -ᵥ p) ↔ z ∈ affineSegment R x y
⊢ z -ᵥ p ∈ affineSegment R (x -ᵥ p) (y -ᵥ p) ↔ z ∈ affineSegment R x y
have rw₁ : z ∈ affineSegment R x y ↔ z ∈ affineSegment R x y
Tactic: rw [← affineSegment_vsub_const_image, (vsub_left_injective p).mem_set_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : IsOrderedRing R
x y : V
⊢ affineSegment R x y = segment R x y
have rw : affineSegment R x y = Set.image.{u_1, u_2} (α := R) (⇑(lineMap x y) : (a : R) → V) (Set.Icc 0 1)
Tactic: rw [segment_eq_image_lineMap, affineSegment]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : IsOrderedRing R
x y : V
rw : affineSegment R x y = Set.image.{u_1, u_2} (α := R) (⇑(lineMap x y) : (a : R) → V) (Set.Icc 0 1)
⊢ affineSegment R x y = segment R x y
have rw₁ : Eq.{u_2 + 1} (α := Set V) (Set.image.{u_1, u_2} (α := R) (⇑(lineMap x y) : (a : R) → V) (Set.Icc 0 1))
  (Set.image.{u_1, u_2} (α := R) (⇑(lineMap x y) : (a : R) → V) (Set.Icc 0 1))
Tactic: rw [segment_eq_image_lineMap, affineSegment]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y : P
⊢ affineSegment R x y = affineSegment R y x
have refine : ∀ (z : P), z ∈ affineSegment R x y ↔ z ∈ affineSegment R y x
Tactic: refine Set.ext fun z => ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
⊢ z ∈ affineSegment R x y ↔ z ∈ affineSegment R y x
have mp : z ∈ affineSegment R x y → z ∈ affineSegment R y x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
mp : z ∈ affineSegment R x y → z ∈ affineSegment R y x
⊢ z ∈ affineSegment R x y ↔ z ∈ affineSegment R y x
have mpr : z ∈ affineSegment R y x → z ∈ affineSegment R x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hxy : (lineMap x y : (a : R) → P) t = z
⊢ z ∈ affineSegment R y x
have mp : Membership.mem (γ := Set R) (Set.Icc 0 1) (1 - t)
Tactic: refine ⟨1 - t, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hxy : (lineMap x y : (a : R) → P) t = z
mp : Membership.mem (γ := Set R) (Set.Icc 0 1) (1 - t)
⊢ z ∈ affineSegment R y x
have mp₁ : (lineMap y x : (a : R) → P) (1 - t) = z
Tactic: refine ⟨1 - t, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hxy : (lineMap x y : (a : R) → P) t = z
⊢ Membership.mem (γ := Set R) (Set.Icc 0 1) (1 - t)
have mp : t ∈ Set.Icc (HSub.hSub (α := R) 1 1) (HSub.hSub (α := R) 1 0)
Tactic: rwa [Set.sub_mem_Icc_iff_right, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hxy : (lineMap x y : (a : R) → P) t = z
mp : t ∈ Set.Icc (HSub.hSub (α := R) 1 1) (HSub.hSub (α := R) 1 0)
⊢ Membership.mem (γ := Set R) (Set.Icc 0 1) (1 - t)
have mp₁ : t ∈ Set.Icc 0 (HSub.hSub (α := R) 1 0)
Tactic: rwa [Set.sub_mem_Icc_iff_right, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hxy : (lineMap y x : (a : R) → P) t = z
⊢ z ∈ affineSegment R x y
have mpr : Membership.mem (γ := Set R) (Set.Icc 0 1) (1 - t)
Tactic: refine ⟨1 - t, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hxy : (lineMap y x : (a : R) → P) t = z
mpr : Membership.mem (γ := Set R) (Set.Icc 0 1) (1 - t)
⊢ z ∈ affineSegment R x y
have mpr₁ : (lineMap x y : (a : R) → P) (1 - t) = z
Tactic: refine ⟨1 - t, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hxy : (lineMap y x : (a : R) → P) t = z
⊢ Membership.mem (γ := Set R) (Set.Icc 0 1) (1 - t)
have mpr : t ∈ Set.Icc (HSub.hSub (α := R) 1 1) (HSub.hSub (α := R) 1 0)
Tactic: rwa [Set.sub_mem_Icc_iff_right, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hxy : (lineMap y x : (a : R) → P) t = z
mpr : t ∈ Set.Icc (HSub.hSub (α := R) 1 1) (HSub.hSub (α := R) 1 0)
⊢ Membership.mem (γ := Set R) (Set.Icc 0 1) (1 - t)
have mpr₁ : t ∈ Set.Icc 0 (HSub.hSub (α := R) 1 0)
Tactic: rwa [Set.sub_mem_Icc_iff_right, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x : P
⊢ affineSegment R x x = {x}
have simp_rw : Eq (α := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x x) : (a : R) → P) (Set.Icc 0 1)) {x}
Tactic: simp_rw [affineSegment, lineMap_same, AffineMap.coe_const, Function.const,
    (Set.nonempty_Icc.mpr zero_le_one).image_const]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x : P
simp_rw : Eq (α := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x x) : (a : R) → P) (Set.Icc 0 1)) {x}
⊢ affineSegment R x x = {x}
have simp_rw₁ : Eq (α := Set P) ((fun (a : R) ↦ (const R R x : (a : R) → P) a) '' Set.Icc 0 1) {x}
Tactic: simp_rw [affineSegment, lineMap_same, AffineMap.coe_const, Function.const,
    (Set.nonempty_Icc.mpr zero_le_one).image_const]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x : P
simp_rw : Eq (α := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x x) : (a : R) → P) (Set.Icc 0 1)) {x}
simp_rw₁ : Eq (α := Set P) ((fun (a : R) ↦ (const R R x : (a : R) → P) a) '' Set.Icc 0 1) {x}
⊢ affineSegment R x x = {x}
have simp_rw₂ : Eq (α := Set P) ((fun (a : R) ↦ Function.const R x a) '' Set.Icc 0 1) {x}
Tactic: simp_rw [affineSegment, lineMap_same, AffineMap.coe_const, Function.const,
    (Set.nonempty_Icc.mpr zero_le_one).image_const]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x : P
simp_rw : Eq (α := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x x) : (a : R) → P) (Set.Icc 0 1)) {x}
simp_rw₁ : Eq (α := Set P) ((fun (a : R) ↦ (const R R x : (a : R) → P) a) '' Set.Icc 0 1) {x}
simp_rw₂ : Eq (α := Set P) ((fun (a : R) ↦ Function.const R x a) '' Set.Icc 0 1) {x}
⊢ affineSegment R x x = {x}
have simp_rw₃ : Eq (α := Set P) ((fun (a : R) ↦ x) '' Set.Icc 0 1) {x}
Tactic: simp_rw [affineSegment, lineMap_same, AffineMap.coe_const, Function.const,
    (Set.nonempty_Icc.mpr zero_le_one).image_const]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : IsOrderedRing R
x y z : V
⊢ y ∈ segment R x z ↔ Wbtw R x y z
have rw : y ∈ segment R x z ↔ y ∈ affineSegment R x z
Tactic: rw [Wbtw, affineSegment_eq_segment]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : IsOrderedRing R
x y z : V
rw : y ∈ segment R x z ↔ y ∈ affineSegment R x z
⊢ y ∈ segment R x z ↔ Wbtw R x y z
have rw₁ : y ∈ segment R x z ↔ y ∈ segment R x z
Tactic: rw [Wbtw, affineSegment_eq_segment]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
⊢ Wbtw R x y z ↔ Wbtw R z y x
have rw : y ∈ affineSegment R x z ↔ Wbtw R z y x
Tactic: rw [Wbtw, Wbtw, affineSegment_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
rw : y ∈ affineSegment R x z ↔ Wbtw R z y x
⊢ Wbtw R x y z ↔ Wbtw R z y x
have rw₁ : y ∈ affineSegment R x z ↔ y ∈ affineSegment R z x
Tactic: rw [Wbtw, Wbtw, affineSegment_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
rw : y ∈ affineSegment R x z ↔ Wbtw R z y x
rw₁ : y ∈ affineSegment R x z ↔ y ∈ affineSegment R z x
⊢ Wbtw R x y z ↔ Wbtw R z y x
have rw₂ : y ∈ affineSegment R z x ↔ y ∈ affineSegment R z x
Tactic: rw [Wbtw, Wbtw, affineSegment_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
⊢ Sbtw R x y z ↔ Sbtw R z y x
have rw : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Sbtw R z y x
Tactic: rw [Sbtw, Sbtw, wbtw_comm, ← and_assoc, ← and_assoc, and_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
rw : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Sbtw R z y x
⊢ Sbtw R x y z ↔ Sbtw R z y x
have rw₁ : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R z y x ∧ y ≠ z ∧ y ≠ x
Tactic: rw [Sbtw, Sbtw, wbtw_comm, ← and_assoc, ← and_assoc, and_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
rw : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Sbtw R z y x
rw₁ : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R z y x ∧ y ≠ z ∧ y ≠ x
⊢ Sbtw R x y z ↔ Sbtw R z y x
have rw₂ : Wbtw R z y x ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R z y x ∧ y ≠ z ∧ y ≠ x
Tactic: rw [Sbtw, Sbtw, wbtw_comm, ← and_assoc, ← and_assoc, and_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
rw : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Sbtw R z y x
rw₁ : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R z y x ∧ y ≠ z ∧ y ≠ x
rw₂ : Wbtw R z y x ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R z y x ∧ y ≠ z ∧ y ≠ x
⊢ Sbtw R x y z ↔ Sbtw R z y x
have rw₃ : (Wbtw R z y x ∧ y ≠ x) ∧ y ≠ z ↔ Wbtw R z y x ∧ y ≠ z ∧ y ≠ x
Tactic: rw [Sbtw, Sbtw, wbtw_comm, ← and_assoc, ← and_assoc, and_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
rw : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Sbtw R z y x
rw₁ : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R z y x ∧ y ≠ z ∧ y ≠ x
rw₂ : Wbtw R z y x ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R z y x ∧ y ≠ z ∧ y ≠ x
rw₃ : (Wbtw R z y x ∧ y ≠ x) ∧ y ≠ z ↔ Wbtw R z y x ∧ y ≠ z ∧ y ≠ x
⊢ Sbtw R x y z ↔ Sbtw R z y x
have rw₄ : (Wbtw R z y x ∧ y ≠ x) ∧ y ≠ z ↔ (Wbtw R z y x ∧ y ≠ z) ∧ y ≠ x
Tactic: rw [Sbtw, Sbtw, wbtw_comm, ← and_assoc, ← and_assoc, and_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
rw : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Sbtw R z y x
rw₁ : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R z y x ∧ y ≠ z ∧ y ≠ x
rw₂ : Wbtw R z y x ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R z y x ∧ y ≠ z ∧ y ≠ x
rw₃ : (Wbtw R z y x ∧ y ≠ x) ∧ y ≠ z ↔ Wbtw R z y x ∧ y ≠ z ∧ y ≠ x
rw₄ : (Wbtw R z y x ∧ y ≠ x) ∧ y ≠ z ↔ (Wbtw R z y x ∧ y ≠ z) ∧ y ≠ x
⊢ Sbtw R x y z ↔ Sbtw R z y x
have rw₅ : (Wbtw R z y x ∧ y ≠ z) ∧ y ≠ x ↔ (Wbtw R z y x ∧ y ≠ z) ∧ y ≠ x
Tactic: rw [Sbtw, Sbtw, wbtw_comm, ← and_assoc, ← and_assoc, and_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
s : AffineSubspace R P
x y z : P
hxyz : Wbtw R x y z
hx : x ∈ s
hz : z ∈ s
⊢ y ∈ s
have obtain : ∀ (ε : R), Membership.mem (α := P) s ((lineMap x z : (a : R) → P) ε : P)
Tactic: obtain ⟨ε, -, rfl⟩ := hxyz
Cleared hypotheses: y, hxyz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
h : Wbtw R x y z
f : P →ᵃ[R] P'
⊢ Wbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P')
have rw : Membership.mem.{u_5, u_5} (α := P') (γ := Set P') ((⇑f : (a : P) → P') '' affineSegment R x z)
  ((f : (a : P) → P') y : P')
Tactic: rw [Wbtw, ← affineSegment_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
hf : Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
⊢ Wbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P') ↔
    Wbtw R x y z
have refine : ∀
  (h :
    Wbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P')
      ((f : (a : P) → P') z : P')),
  Wbtw R x y z
Tactic: refine ⟨fun h => ?_, fun h => h.map _⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
hf : Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
h : Wbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P')
⊢ Wbtw R x y z
have rwa : ∀
  (h :
    Membership.mem.{u_5, u_5} (α := P') (γ := Set P')
      (affineSegment R ((f : (a : P) → P') x) ((f : (a : P) → P') z) : Set P') ((f : (a : P) → P') y : P')),
  Wbtw R x y z
Tactic: rwa [Wbtw, ← affineSegment_image, hf.mem_set_image] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
hf : Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
h : Wbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P')
rwa :
  ∀
    (h :
      Membership.mem.{u_5, u_5} (α := P') (γ := Set P')
        (affineSegment R ((f : (a : P) → P') x) ((f : (a : P) → P') z) : Set P') ((f : (a : P) → P') y : P')),
    Wbtw R x y z
⊢ Wbtw R x y z
have rwa₁ : ∀
  (h :
    Membership.mem.{u_5, u_5} (α := P') (γ := Set P') ((⇑f : (a : P) → P') '' affineSegment R x z)
      ((f : (a : P) → P') y : P')),
  Wbtw R x y z
Tactic: rwa [Wbtw, ← affineSegment_image, hf.mem_set_image] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
hf : Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
h : Wbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P')
rwa :
  ∀
    (h :
      Membership.mem.{u_5, u_5} (α := P') (γ := Set P')
        (affineSegment R ((f : (a : P) → P') x) ((f : (a : P) → P') z) : Set P') ((f : (a : P) → P') y : P')),
    Wbtw R x y z
rwa₁ :
  ∀
    (h :
      Membership.mem.{u_5, u_5} (α := P') (γ := Set P') ((⇑f : (a : P) → P') '' affineSegment R x z)
        ((f : (a : P) → P') y : P')),
    Wbtw R x y z
⊢ Wbtw R x y z
have rwa₂ : ∀ (h : y ∈ affineSegment R x z), Wbtw R x y z
Tactic: rwa [Wbtw, ← affineSegment_image, hf.mem_set_image] at h
Cleared hypotheses: h