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 : P
rw : Wbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ∧ y -ᵥ p ≠ x -ᵥ p ∧ y -ᵥ p ≠ z -ᵥ p ↔ Sbtw R x y z
rw₁ : Wbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ∧ y -ᵥ p ≠ x -ᵥ p ∧ y -ᵥ p ≠ z -ᵥ p ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
rw₂ : Wbtw R x y z ∧ y -ᵥ p ≠ x -ᵥ p ∧ y -ᵥ p ≠ z -ᵥ p ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
rw₃ : Wbtw R x y z ∧ y ≠ x ∧ y -ᵥ p ≠ z -ᵥ p ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
⊢ Sbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Sbtw R x y z
have rw₄ : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Tactic: rw [Sbtw, Sbtw, wbtw_vsub_const_iff, (vsub_left_injective p).ne_iff,
    (vsub_left_injective p).ne_iff]
-- 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
h : Sbtw R x y z
⊢ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x z) : (a : R) → P) (Set.Ioo 0 1)) y
have rcases : ∀ (t : R) (ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t) (hyx : (lineMap x z : (a : R) → P) t ≠ x)
  (hyz : (lineMap x z : (a : R) → P) t ≠ z),
  Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x z) : (a : R) → P) (Set.Ioo 0 1)) ((lineMap x z : (a : R) → P) t : P)
Tactic: rcases h with ⟨⟨t, ht, rfl⟩, hyx, hyz⟩
Cleared hypotheses: y, h
-- 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 z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hyx : (lineMap x z : (a : R) → P) t ≠ x
hyz : (lineMap x z : (a : R) → P) t ≠ z
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x z) : (a : R) → P) (Set.Ioo 0 1)) ((lineMap x z : (a : R) → P) t : P)
have inl : ∀ (ht : Membership.mem (γ := Set R) (Set.Icc 0 1) 0) (hyx : (lineMap x z : (a : R) → P) 0 ≠ x)
  (hyz : (lineMap x z : (a : R) → P) 0 ≠ z),
  Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x z) : (a : R) → P) (Set.Ioo 0 1)) ((lineMap x z : (a : R) → P) 0 : P)
Tactic: rcases Set.eq_endpoints_or_mem_Ioo_of_mem_Icc ht with (rfl | rfl | ho)
Cleared hypotheses: t, ht, hyx, hyz
-- 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 z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hyx : (lineMap x z : (a : R) → P) t ≠ x
hyz : (lineMap x z : (a : R) → P) t ≠ z
inl :
  ∀ (ht : Membership.mem (γ := Set R) (Set.Icc 0 1) 0) (hyx : (lineMap x z : (a : R) → P) 0 ≠ x)
    (hyz : (lineMap x z : (a : R) → P) 0 ≠ z),
    Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x z) : (a : R) → P) (Set.Ioo 0 1)) ((lineMap x z : (a : R) → P) 0 : P)
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x z) : (a : R) → P) (Set.Ioo 0 1)) ((lineMap x z : (a : R) → P) t : P)
have inr : ∀ (ht : Membership.mem (γ := Set R) (Set.Icc 0 1) 1) (hyx : (lineMap x z : (a : R) → P) 1 ≠ x)
  (hyz : (lineMap x z : (a : R) → P) 1 ≠ z),
  Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x z) : (a : R) → P) (Set.Ioo 0 1)) ((lineMap x z : (a : R) → P) 1 : P)
Tactic: rcases Set.eq_endpoints_or_mem_Ioo_of_mem_Icc ht with (rfl | rfl | ho)
Cleared hypotheses: t, ht, hyx, hyz
-- 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 z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hyx : (lineMap x z : (a : R) → P) t ≠ x
hyz : (lineMap x z : (a : R) → P) t ≠ z
inl :
  ∀ (ht : Membership.mem (γ := Set R) (Set.Icc 0 1) 0) (hyx : (lineMap x z : (a : R) → P) 0 ≠ x)
    (hyz : (lineMap x z : (a : R) → P) 0 ≠ z),
    Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x z) : (a : R) → P) (Set.Ioo 0 1)) ((lineMap x z : (a : R) → P) 0 : P)
inr :
  ∀ (ht : Membership.mem (γ := Set R) (Set.Icc 0 1) 1) (hyx : (lineMap x z : (a : R) → P) 1 ≠ x)
    (hyz : (lineMap x z : (a : R) → P) 1 ≠ z),
    Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x z) : (a : R) → P) (Set.Ioo 0 1)) ((lineMap x z : (a : R) → P) 1 : P)
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x z) : (a : R) → P) (Set.Ioo 0 1)) ((lineMap x z : (a : R) → P) t : P)
have inr₁ : ∀ (ho : Membership.mem (γ := Set R) (Set.Ioo 0 1) t),
  Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x z) : (a : R) → P) (Set.Ioo 0 1)) ((lineMap x z : (a : R) → P) t : P)
Tactic: rcases Set.eq_endpoints_or_mem_Ioo_of_mem_Icc ht with (rfl | rfl | ho)
-- 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 z : P
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) 0
hyx : (lineMap x z : (a : R) → P) 0 ≠ x
hyz : (lineMap x z : (a : R) → P) 0 ≠ z
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x z) : (a : R) → P) (Set.Ioo 0 1)) ((lineMap x z : (a : R) → P) 0 : P)
have inl : False
Tactic: exfalso
-- 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 z : P
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) 1
hyx : (lineMap x z : (a : R) → P) 1 ≠ x
hyz : (lineMap x z : (a : R) → P) 1 ≠ z
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x z) : (a : R) → P) (Set.Ioo 0 1)) ((lineMap x z : (a : R) → P) 1 : P)
have inr : False
Tactic: exfalso
-- 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
h : Wbtw R x y z
⊢ Membership.mem (γ := AffineSubspace R P) (affineSpan R {x, z}) y
have rcases : ∀ (r : R), Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R {x, z}) ((lineMap x z : (a : R) → P) r : P)
Tactic: rcases h with ⟨r, ⟨-, rfl⟩⟩
Cleared hypotheses: y, h
-- 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
⊢ Wbtw R x y x ↔ y = x
have refine_1 : ∀ (h : Wbtw R x y x), y = x
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- 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
refine_1 : ∀ (h : Wbtw R x y x), y = x
⊢ Wbtw R x y x ↔ y = x
have refine_2 : ∀ (h : y = x), Wbtw R x y x
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- 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
h : y = x
⊢ Wbtw R x y x
have refine_2 : Wbtw R x x x
Tactic: rw [h]
-- 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 : ZeroLEOneClass R
R' : Type u_6
inst_6 : Ring R'
inst_7 : PartialOrder R'
inst_8 : Module R' V
inst_9 : Module R' R
inst_10 : IsScalarTower R' R V
inst_11 : SMulPosMono R' R
x y : P
a : R'
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ Membership.mem (α := P) (affineSegment R x y) ((lineMap x y : (a : R') → P) a : P)
have refine_1 : 0 ≤ HSMul.hSMul (β := R) a 1
Tactic: refine ⟨a • 1, ⟨?_, ?_⟩, by simp [lineMap_apply]⟩
-- 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 : ZeroLEOneClass R
R' : Type u_6
inst_6 : Ring R'
inst_7 : PartialOrder R'
inst_8 : Module R' V
inst_9 : Module R' R
inst_10 : IsScalarTower R' R V
inst_11 : SMulPosMono R' R
x y : P
a : R'
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
refine_1 : 0 ≤ HSMul.hSMul (β := R) a 1
⊢ Membership.mem (α := P) (affineSegment R x y) ((lineMap x y : (a : R') → P) a : P)
have refine_2 : HSMul.hSMul (β := R) a 1 ≤ 1
Tactic: refine ⟨a • 1, ⟨?_, ?_⟩, by simp [lineMap_apply]⟩
-- 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 : ZeroLEOneClass R
R' : Type u_6
inst_6 : Ring R'
inst_7 : PartialOrder R'
inst_8 : Module R' V
inst_9 : Module R' R
inst_10 : IsScalarTower R' R V
inst_11 : SMulPosMono R' R
x y : P
a : R'
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ 0 ≤ HSMul.hSMul (β := R) a 1
have refine_1 : HSMul.hSMul.{u_6, u_1, u_1} (α := R') (β := R) 0 1 ≤ HSMul.hSMul (β := R) a 1
Tactic: rw [← zero_smul R' (1 : R)]
-- 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 : ZeroLEOneClass R
R' : Type u_6
inst_6 : Ring R'
inst_7 : PartialOrder R'
inst_8 : Module R' V
inst_9 : Module R' R
inst_10 : IsScalarTower R' R V
inst_11 : SMulPosMono R' R
x y : P
a : R'
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ HSMul.hSMul (β := R) a 1 ≤ 1
have refine_2 : HSMul.hSMul (β := R) a 1 ≤ HSMul.hSMul.{u_6, u_1, u_1} (α := R') (β := R) 1 1
Tactic: nth_rw 2 [← one_smul R' 1]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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
hne : y ≠ x
h : Wbtw R x y x
⊢ False
have h₁ : y = x
Tactic: rw [wbtw_self_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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
h : Wbtw R x y x
hne : y ≠ x
⊢ False
have h₁ : y = x
Tactic: rw [wbtw_self_iff] at h
Cleared hypotheses: h, hne
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
x : R
⊢ (∃ (x_1 : R), Membership.mem (γ := Set R) (Set.Icc 0 1) x_1 ∧ (lineMap 0 1 : (a : R) → R) x_1 = x) ↔
    Membership.mem (γ := Set R) (Set.Icc 0 1) x
have simp_rw : (∃ (x_1 : R), Membership.mem (γ := Set R) (Set.Icc 0 1) x_1 ∧ (1 - x_1) * 0 + x_1 * 1 = x) ↔
  Membership.mem (γ := Set R) (Set.Icc 0 1) x
Tactic: simp_rw [lineMap_apply_ring]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
⊢ Wbtw R 1 x 0 ↔ Membership.mem (γ := Set R) (Set.Icc 0 1) x
have rw : Wbtw R 0 x 1 ↔ Membership.mem (γ := Set R) (Set.Icc 0 1) x
Tactic: rw [wbtw_comm, wbtw_zero_one_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
rw : Wbtw R 0 x 1 ↔ Membership.mem (γ := Set R) (Set.Icc 0 1) x
⊢ Wbtw R 1 x 0 ↔ Membership.mem (γ := Set R) (Set.Icc 0 1) x
have rw₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) x ↔ Membership.mem (γ := Set R) (Set.Icc 0 1) x
Tactic: rw [wbtw_comm, wbtw_zero_one_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
x : R
⊢ Sbtw R 0 x 1 ↔ Membership.mem (γ := Set R) (Set.Ioo 0 1) x
have rw : (0 ≤ x ∧ x ≤ 1) ∧ x ≠ 0 ∧ x ≠ 1 ↔ 0 < x ∧ x < 1
Tactic: rw [Sbtw, wbtw_zero_one_iff, Set.mem_Icc, Set.mem_Ioo]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
⊢ Sbtw R 1 x 0 ↔ Membership.mem (γ := Set R) (Set.Ioo 0 1) x
have rw : Sbtw R 0 x 1 ↔ Membership.mem (γ := Set R) (Set.Ioo 0 1) x
Tactic: rw [sbtw_comm, sbtw_zero_one_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
rw : Sbtw R 0 x 1 ↔ Membership.mem (γ := Set R) (Set.Ioo 0 1) x
⊢ Sbtw R 1 x 0 ↔ Membership.mem (γ := Set R) (Set.Ioo 0 1) x
have rw₁ : Membership.mem (γ := Set R) (Set.Ioo 0 1) x ↔ Membership.mem (γ := Set R) (Set.Ioo 0 1) x
Tactic: rw [sbtw_comm, sbtw_zero_one_iff]
-- 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
w x y z : P
h₁ : Wbtw R w y z
h₂ : Wbtw R w x y
⊢ Wbtw R w x z
have rcases : ∀ (t₁ : R) (ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁) (h₂ : Wbtw R w x ((lineMap w z : (a : R) → P) t₁)),
  Wbtw R w x z
Tactic: rcases h₁ with ⟨t₁, ht₁, rfl⟩
Cleared hypotheses: y, h₁, h₂
-- 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
w x z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
h₂ : Wbtw R w x ((lineMap w z : (a : R) → P) t₁)
⊢ Wbtw R w x z
have rcases : ∀ (t₂ : R) (ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂),
  Wbtw R w ((lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂) z
Tactic: rcases h₂ with ⟨t₂, ht₂, rfl⟩
Cleared hypotheses: x, h₂
-- 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
w z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
⊢ Wbtw R w ((lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂) z
have refine : Eq.{u_4 + 1} (α := P) ((lineMap w z : (a : R) → P) (t₂ * t₁) : P)
  ((lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂ : P)
Tactic: refine ⟨t₂ * t₁, ⟨mul_nonneg ht₂.1 ht₁.1, mul_le_one₀ ht₂.2 ht₁.1 ht₁.2⟩, ?_⟩
-- 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
w z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
⊢ Eq.{u_4 + 1} (α := P) ((lineMap w z : (a : R) → P) (t₂ * t₁) : P)
    ((lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂ : P)
have rw : (t₂ * t₁) • (z -ᵥ w) +ᵥ w = (lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂
Tactic: rw [lineMap_apply, lineMap_apply, lineMap_vsub_left, smul_smul]
-- 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
w z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
rw : (t₂ * t₁) • (z -ᵥ w) +ᵥ w = (lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂
⊢ Eq.{u_4 + 1} (α := P) ((lineMap w z : (a : R) → P) (t₂ * t₁) : P)
    ((lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂ : P)
have rw₁ : (t₂ * t₁) • (z -ᵥ w) +ᵥ w = t₂ • ((lineMap w z : (a : R) → P) t₁ -ᵥ w) +ᵥ w
Tactic: rw [lineMap_apply, lineMap_apply, lineMap_vsub_left, smul_smul]
-- 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
w z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
rw : (t₂ * t₁) • (z -ᵥ w) +ᵥ w = (lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂
rw₁ : (t₂ * t₁) • (z -ᵥ w) +ᵥ w = t₂ • ((lineMap w z : (a : R) → P) t₁ -ᵥ w) +ᵥ w
⊢ Eq.{u_4 + 1} (α := P) ((lineMap w z : (a : R) → P) (t₂ * t₁) : P)
    ((lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂ : P)
have rw₂ : (t₂ * t₁) • (z -ᵥ w) +ᵥ w = t₂ • t₁ • (z -ᵥ w) +ᵥ w
Tactic: rw [lineMap_apply, lineMap_apply, lineMap_vsub_left, smul_smul]
-- 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
w z : P
t₁ : R
ht₁ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₁
t₂ : R
ht₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) t₂
rw : (t₂ * t₁) • (z -ᵥ w) +ᵥ w = (lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂
rw₁ : (t₂ * t₁) • (z -ᵥ w) +ᵥ w = t₂ • ((lineMap w z : (a : R) → P) t₁ -ᵥ w) +ᵥ w
rw₂ : (t₂ * t₁) • (z -ᵥ w) +ᵥ w = t₂ • t₁ • (z -ᵥ w) +ᵥ w
⊢ Eq.{u_4 + 1} (α := P) ((lineMap w z : (a : R) → P) (t₂ * t₁) : P)
    ((lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂ : P)
have rw₃ : (t₂ * t₁) • (z -ᵥ w) +ᵥ w = (t₂ * t₁) • (z -ᵥ w) +ᵥ w
Tactic: rw [lineMap_apply, lineMap_apply, lineMap_vsub_left, smul_smul]
-- 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
w x y z : P
h₁ : Wbtw R w x z
h₂ : Wbtw R x y z
⊢ Wbtw R w y z
have rw : ∀ (h₁ : Wbtw R z x w) (h₂ : Wbtw R z y x), Wbtw R z y w
Tactic: rw [wbtw_comm] at *
Cleared hypotheses: h₁, h₂
-- 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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
⊢ Sbtw R x y z ↔
    Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x z) : (a : R) → P) (Set.Ioo 0 1)) y ∧ x ≠ z
have refine : ∀
  (h :
    Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x z) : (a : R) → P) (Set.Ioo 0 1)) y ∧ x ≠ z),
  Sbtw R x y z
Tactic: refine ⟨fun h => ⟨h.mem_image_Ioo, h.left_ne_right⟩, fun h => ?_⟩
-- 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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
h : Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x z) : (a : R) → P) (Set.Ioo 0 1)) y ∧ x ≠ z
⊢ Sbtw R x y z
have rcases : ∀ (hxz : x ≠ z) (t : R) (ht : Membership.mem (γ := Set R) (Set.Ioo 0 1) t), Sbtw R x ((lineMap x z : (a : R) → P) t) z
Tactic: rcases h with ⟨⟨t, ht, rfl⟩, hxz⟩
Cleared hypotheses: y, h
-- 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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x z : P
hxz : x ≠ z
t : R
ht : Membership.mem (γ := Set R) (Set.Ioo 0 1) t
⊢ Sbtw R x ((lineMap x z : (a : R) → P) t) z
have refine : (lineMap x z : (a : R) → P) t ≠ x ∧ (lineMap x z : (a : R) → P) t ≠ z
Tactic: refine ⟨⟨t, Set.mem_Icc_of_Ioo ht, rfl⟩, ?_⟩
-- 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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x z : P
hxz : x ≠ z
t : R
ht : Membership.mem (γ := Set R) (Set.Ioo 0 1) t
⊢ (lineMap x z : (a : R) → P) t ≠ x ∧ (lineMap x z : (a : R) → P) t ≠ z
have rw : t • (z -ᵥ x) + 0 ≠ 0 ∧ (t - 1) • (z -ᵥ x) ≠ 0
Tactic: rw [lineMap_apply, ← @vsub_ne_zero V, ← @vsub_ne_zero V _ _ _ _ z, vadd_vsub_assoc, vsub_self,
    vadd_vsub_assoc, ← neg_vsub_eq_vsub_rev z x, ← @neg_one_smul R, ← add_smul, ← sub_eq_add_neg]
-- 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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
⊢ Wbtw R x y z ∧ Wbtw R y x z ↔ x = y
have mp : Wbtw R x y z ∧ Wbtw R y x z → 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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
mp : Wbtw R x y z ∧ Wbtw R y x z → x = y
⊢ Wbtw R x y z ∧ Wbtw R y x z ↔ x = y
have mpr : x = y → Wbtw R x y z ∧ Wbtw R y x z
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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
hxyz : Wbtw R x y z
hyxz : Wbtw R y x z
⊢ x = y
have mp : ∀ (ty : R) (hty : Membership.mem (γ := Set R) (Set.Icc 0 1) ty) (hyxz : Wbtw R ((lineMap x z : (a : R) → P) ty) x z),
  x = (lineMap x z : (a : R) → P) ty
Tactic: rcases hxyz with ⟨ty, hty, rfl⟩
Cleared hypotheses: y, hxyz, hyxz
-- 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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x z : P
ty : R
hty : Membership.mem (γ := Set R) (Set.Icc 0 1) ty
hyxz : Wbtw R ((lineMap x z : (a : R) → P) ty) x z
⊢ x = (lineMap x z : (a : R) → P) ty
have mp : ∀ (tx : R) (htx : Membership.mem (γ := Set R) (Set.Icc 0 1) tx)
  (hx : ((lineMap ((lineMap x z : (a : R) → P) ty) z : R →ᵃ[R] P) : (a : R) → P) tx = x),
  x = (lineMap x z : (a : R) → P) ty
Tactic: rcases hyxz with ⟨tx, htx, hx⟩
Cleared hypotheses: hyxz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x z : P
ty : R
hty : Membership.mem (γ := Set R) (Set.Icc 0 1) ty
tx : R
htx : Membership.mem (γ := Set R) (Set.Icc 0 1) tx
hx : ((lineMap ((lineMap x z : (a : R) → P) ty) z : R →ᵃ[R] P) : (a : R) → P) tx = x
⊢ x = (lineMap x z : (a : R) → P) ty
have hx₁ : (tx • (z -ᵥ (ty • (z -ᵥ x) +ᵥ x)) + ty • (z -ᵥ x)) +ᵥ x = x
Tactic: rw [lineMap_apply, lineMap_apply, ← add_vadd] at hx
Cleared hypotheses: hx