awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x y z : R
hxz : x ≤ z
⊢ x = z ∨ x < z

Tactic:
cases hxz.eq_or_lt with
  | inl hxz =>
    subst hxz
    rw [← le_antisymm_iff, wbtw_self_iff, eq_comm]
  | inr hxz =>
    have hxz' : 0 < z - x := sub_pos.mpr hxz
    let r := (y - x) / (z - x)
    have hy : y = r * (z - x) + x := by simp [r, hxz'.ne']
    simp [hy, wbtw_mul_sub_add_iff, mul_nonneg_iff_of_pos_right hxz', ← le_sub_iff_add_le,
      mul_le_iff_le_one_left hxz', hxz.ne]

Premises used: LE.le.eq_or_lt, eq_comm, wbtw_self_iff, le_antisymm_iff, le_sub_iff_add_le, wbtw_mul_sub_add_iff
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x y z : R
hxy : x ≤ y
hyz : y ≤ z
⊢ Wbtw R x y z

Tactic:
(wbtw_iff_of_le (hxy.trans hyz)).mpr ⟨hxy, hyz⟩

Premises used: Iff.mpr, And.intro, LE.le.trans, wbtw_iff_of_le
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x y z : R
hxy : x < y
hyz : y < z
⊢ Sbtw R x y z

Tactic:
⟨.of_le_of_le hxy.le hyz.le, hxy.ne', hyz.ne⟩

Premises used: LT.lt.le, Wbtw.of_le_of_le, LT.lt.ne', And.intro, Sbtw, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
⊢ Wbtw R x y z ↔
    x = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ici 1)) z

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

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
refine_1 :
  ∀ (h : Wbtw R x y z),
    x = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ici 1)) z
refine_2 :
  ∀
    (h :
      x = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ici 1)) z),
    Wbtw R x y z
⊢ Wbtw R x y z ↔
    x = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ici 1)) z

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
h : Wbtw R x y z
refine_1 :
  ∀ (r : R) (hr0 : 0 ≤ r) (hr1 : r ≤ 1),
    x = (lineMap x z : (a : R) → P) r ∨
      Membership.mem (γ := Set P)
        (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x ((lineMap x z : (a : R) → P) r)) : (a : R) → P) (Set.Ici 1)) z
⊢ x = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ici 1)) z

Tactic:
rcases h with ⟨r, ⟨hr0, hr1⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
refine_1 :
  ∀ (hr0' : 0 < r),
    x = (lineMap x z : (a : R) → P) r ∨
      Membership.mem (γ := Set P)
        (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x ((lineMap x z : (a : R) → P) r)) : (a : R) → P) (Set.Ici 1)) z
refine_1₁ :
  ∀ (hr0 : LE.le.{u_1} (α := R) 0 0) (hr1 : LE.le.{u_1} (α := R) 0 1),
    x = (lineMap x z : (a : R) → P) 0 ∨
      Membership.mem (γ := Set P)
        (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x ((lineMap x z : (a : R) → P) 0)) : (a : R) → P) (Set.Ici 1)) z
⊢ x = (lineMap x z : (a : R) → P) r ∨
    Membership.mem (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x ((lineMap x z : (a : R) → P) r)) : (a : R) → P) (Set.Ici 1)) z

Tactic:
rcases hr0.lt_or_eq with (hr0' | rfl)

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ x = (lineMap x z : (a : R) → P) r ∨
    ∃ (x_1 : R),
      Membership.mem (γ := Set R) (Set.Ici 1) x_1 ∧ (lineMap x ((lineMap x z : (a : R) → P) r) : (a : R) → P) x_1 = z

Tactic:
.inr ⟨r⁻¹, (one_le_inv₀ hr0').2 hr1, ?_⟩

Premises used: Iff.mpr, one_le_inv₀, Inv.inv, And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
refine_1 : (lineMap x ((lineMap x z : (a : R) → P) r) : (a : R) → P) r⁻¹ = z
⊢ x = (lineMap x z : (a : R) → P) r ∨
    ∃ (x_1 : R),
      Membership.mem (γ := Set R) (Set.Ici 1) x_1 ∧ (lineMap x ((lineMap x z : (a : R) → P) r) : (a : R) → P) x_1 = z

Tactic:
refine .inr ⟨r⁻¹, (one_le_inv₀ hr0').2 hr1, ?_⟩
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
refine_1 : (r⁻¹ * r) • (z -ᵥ x) +ᵥ x = z
⊢ (lineMap x ((lineMap x z : (a : R) → P) r) : (a : R) → P) r⁻¹ = z

Tactic:
simp only [lineMap_apply, smul_smul, vadd_vsub]

Premises used: smul_smul, AffineMap.lineMap_apply, vadd_vsub
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
refine_1 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (z -ᵥ x) +ᵥ x = z
refine_1₁ : (z -ᵥ x) +ᵥ x = z
refine_1₂ refine_1₃ : z = z
⊢ (r⁻¹ * r) • (z -ᵥ x) +ᵥ x = z

Tactic:
rw [inv_mul_cancel₀ hr0'.ne', one_smul, vsub_vadd]

Premises used: one_smul, LT.lt.ne', vsub_vadd, inv_mul_cancel₀
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x z : P
hr0 : LE.le.{u_1} (α := R) 0 0
hr1 : LE.le.{u_1} (α := R) 0 1
⊢ x = (lineMap x z : (a : R) → P) 0 ∨
    Membership.mem (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x ((lineMap x z : (a : R) → P) 0)) : (a : R) → P) (Set.Ici 1)) z

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
h : x = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ici 1)) z
refine_2 : Wbtw R x x z
refine_2₁ : ∀ (r : R) (hr : Membership.mem (γ := Set R) (Set.Ici 1) r), Wbtw R x y ((lineMap x y : (a : R) → P) r)
⊢ Wbtw R x y z

Tactic:
rcases h with (rfl | ⟨r, ⟨hr, rfl⟩⟩)

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x z : P
⊢ Wbtw R x x z

Tactic:
wbtw_self_left _ _ _

Premises used: wbtw_self_left
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x z : P
⊢ Wbtw R x x z

Tactic:
exact wbtw_self_left _ _ _

Premises used: wbtw_self_left
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
r : R
hr : Membership.mem (γ := Set R) (Set.Ici 1) r
⊢ 1 ≤ r

Tactic:
rw [Set.mem_Ici] at hr

Premises used: Set.mem_Ici
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
⊢ Wbtw R x y ((lineMap x y : (a : R) → P) r)

Tactic:
⟨r⁻¹, ⟨inv_nonneg.2 (zero_le_one.trans hr), inv_le_one_of_one_le₀ hr⟩, ?_⟩

Premises used: affineSegment, Iff.mpr, Set.Mem, Wbtw, setOf, zero_le_one, Inv.inv, inv_nonneg, And.intro, Exists.intro, Set.image, LE.le.trans, inv_le_one_of_one_le₀
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
refine_2 : (lineMap x ((lineMap x y : (a : R) → P) r) : (a : R) → P) r⁻¹ = y
⊢ Wbtw R x y ((lineMap x y : (a : R) → P) r)

Tactic:
refine ⟨r⁻¹, ⟨inv_nonneg.2 (zero_le_one.trans hr), inv_le_one_of_one_le₀ hr⟩, ?_⟩
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
refine_2 : (r⁻¹ * r) • (y -ᵥ x) +ᵥ x = y
⊢ (lineMap x ((lineMap x y : (a : R) → P) r) : (a : R) → P) r⁻¹ = y

Tactic:
simp only [lineMap_apply, smul_smul, vadd_vsub]

Premises used: smul_smul, AffineMap.lineMap_apply, vadd_vsub
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
refine_2 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (y -ᵥ x) +ᵥ x = y
refine_2₁ : (y -ᵥ x) +ᵥ x = y
refine_2₂ refine_2₃ : y = y
⊢ (r⁻¹ * r) • (y -ᵥ x) +ᵥ x = y

Tactic:
rw [inv_mul_cancel₀ (one_pos.trans_le hr).ne', one_smul, vsub_vadd]

Premises used: one_smul, LT.lt.ne', LT.lt.trans_le, vsub_vadd, one_pos, inv_mul_cancel₀
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
h : Wbtw R x y z
hne : x ≠ y
⊢ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ici 1)) z

Tactic:
(wbtw_iff_left_eq_or_right_mem_image_Ici.1 h).resolve_left hne

Premises used: Or.resolve_left, wbtw_iff_left_eq_or_right_mem_image_Ici, Iff.mp
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
h : Wbtw R x y z
hne : x ≠ y
rcases :
  ∀ (r : R) (h : Wbtw R x y ((lineMap x y : (a : R) → P) r)),
    Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R {x, y}) ((lineMap x y : (a : R) → P) r : P)
⊢ Membership.mem (γ := AffineSubspace R P) (affineSpan R {x, y}) z

Tactic:
rcases h.right_mem_image_Ici_of_left_ne hne with ⟨r, ⟨-, rfl⟩⟩

Premises used: Wbtw.right_mem_image_Ici_of_left_ne, rfl
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
hne : x ≠ y
r : R
h : Wbtw R x y ((lineMap x y : (a : R) → P) r)
⊢ Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R {x, y}) ((lineMap x y : (a : R) → P) r : P)

Tactic:
lineMap_mem_affineSpan_pair _ _ _

Premises used: AffineMap.lineMap_mem_affineSpan_pair
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
hne : x ≠ y
r : R
h : Wbtw R x y ((lineMap x y : (a : R) → P) r)
⊢ Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R {x, y}) ((lineMap x y : (a : R) → P) r : P)

Tactic:
exact lineMap_mem_affineSpan_pair _ _ _

Premises used: AffineMap.lineMap_mem_affineSpan_pair
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
⊢ Sbtw R x y z ↔
    x ≠ y ∧ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) z

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

Premises used: And.intro, Iff.intro, Sbtw.left_ne
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
refine_1 :
  ∀ (h : Sbtw R x y z),
    Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) z
refine_2 :
  ∀
    (h :
      x ≠ y ∧ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) z),
    Sbtw R x y z
⊢ Sbtw R x y z ↔
    x ≠ y ∧ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) z

Tactic:
refine ⟨fun h => ⟨h.left_ne, ?_⟩, fun h => ?_⟩
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
h : Sbtw R x y z
refine_1 :
  ∀ (r : R) (hr : Membership.mem (γ := Set R) (Set.Ici 1) r) (h : Sbtw R x y ((lineMap x y : (a : R) → P) r)),
    Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) ((lineMap x y : (a : R) → P) r : P)
⊢ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) z

Tactic:
obtain ⟨r, ⟨hr, rfl⟩⟩ := h.wbtw.right_mem_image_Ici_of_left_ne h.left_ne

Premises used: Wbtw.right_mem_image_Ici_of_left_ne, Sbtw.wbtw, Sbtw.left_ne, rfl
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
r : R
hr : Membership.mem (γ := Set R) (Set.Ici 1) r
h : Sbtw R x y ((lineMap x y : (a : R) → P) r)
⊢ 1 ≤ r

Tactic:
rw [Set.mem_Ici] at hr

Premises used: Set.mem_Ici
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
r : R
hr : Membership.mem (γ := Set R) (Set.Ici 1) r
h : Sbtw R x y ((lineMap x y : (a : R) → P) r)
hr₁ : 1 ≤ r
⊢ Sbtw R x y ((lineMap x y : (a : R) → P) r)

Tactic:
rw [Set.mem_Ici] at hr

Premises used: Set.mem_Ici
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
h : Sbtw R x y ((lineMap x y : (a : R) → P) r)
refine_1 :
  ∀ (hrlt : 1 < r),
    Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) ((lineMap x y : (a : R) → P) r : P)
refine_1₁ :
  ∀ (hr : LE.le.{u_1} (α := R) 1 1) (h : Sbtw R x y ((lineMap x y : (a : R) → P) 1)),
    Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) ((lineMap x y : (a : R) → P) 1 : P)
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) ((lineMap x y : (a : R) → P) r : P)

Tactic:
rcases hr.lt_or_eq with (hrlt | rfl)

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
h : Sbtw R x y ((lineMap x y : (a : R) → P) r)
hrlt : 1 < r
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) ((lineMap x y : (a : R) → P) r : P)

Tactic:
Set.mem_image_of_mem _ hrlt

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
h : Sbtw R x y ((lineMap x y : (a : R) → P) r)
hrlt : 1 < r
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) ((lineMap x y : (a : R) → P) r : P)

Tactic:
exact Set.mem_image_of_mem _ hrlt

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
hr : LE.le.{u_1} (α := R) 1 1
h : Sbtw R x y ((lineMap x y : (a : R) → P) 1)
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) ((lineMap x y : (a : R) → P) 1 : P)

Tactic:
simp at h
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
h : x ≠ y ∧ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) z
refine_2 :
  ∀ (hne : x ≠ y) (r : R) (hr : Membership.mem (γ := Set R) (Set.Ioi 1) r), Sbtw R x y ((lineMap x y : (a : R) → P) r)
⊢ Sbtw R x y z

Tactic:
rcases h with ⟨hne, r, hr, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : Membership.mem (γ := Set R) (Set.Ioi 1) r
⊢ 1 < r

Tactic:
rw [Set.mem_Ioi] at hr

Premises used: Set.mem_Ioi
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ Sbtw R x y ((lineMap x y : (a : R) → P) r)

Tactic:
⟨wbtw_iff_left_eq_or_right_mem_image_Ici.2
          (Or.inr (Set.mem_image_of_mem _ (Set.mem_of_mem_of_subset hr Set.Ioi_subset_Ici_self))),
        hne.symm, ?_⟩

Premises used: Iff.mpr, Set.Ioi_subset_Ici_self, Ne.symm, wbtw_iff_left_eq_or_right_mem_image_Ici, Set.mem_image_of_mem, Set.mem_of_mem_of_subset, And.intro, Sbtw, Or.inr
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
refine_2 : y ≠ (lineMap x y : (a : R) → P) r
⊢ Sbtw R x y ((lineMap x y : (a : R) → P) r)

Tactic:
refine
      ⟨wbtw_iff_left_eq_or_right_mem_image_Ici.2
          (Or.inr (Set.mem_image_of_mem _ (Set.mem_of_mem_of_subset hr Set.Ioi_subset_Ici_self))),
        hne.symm, ?_⟩
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
refine_2 : y -ᵥ x - r • (y -ᵥ x) ≠ 0
⊢ y ≠ (lineMap x y : (a : R) → P) r

Tactic:
rw [lineMap_apply, ← @vsub_ne_zero V, vsub_vadd_eq_vsub_sub]

Premises used: vsub_vadd_eq_vsub_sub, vsub_ne_zero, AffineMap.lineMap_apply
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
refine_2 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (y -ᵥ x) - r • (y -ᵥ x) ≠ 0
⊢ y -ᵥ x - r • (y -ᵥ x) ≠ 0

Tactic:
nth_rw 1 [← one_smul R (y -ᵥ x)]

Premises used: VSub.vsub, one_smul
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
refine_2 : 1 ≠ r ∧ y ≠ x
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (y -ᵥ x) - r • (y -ᵥ x) ≠ 0

Tactic:
rw [← sub_smul, smul_ne_zero_iff, vsub_ne_zero, sub_ne_zero]

Premises used: vsub_ne_zero, sub_ne_zero, sub_smul, smul_ne_zero_iff
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ 1 ≠ r ∧ y ≠ x

Tactic:
⟨hr.ne, hne.symm⟩

Premises used: Ne.symm, And.intro, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ 1 ≠ r ∧ y ≠ x

Tactic:
exact ⟨hr.ne, hne.symm⟩
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : 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 y) : (a : R) → P) (Set.Ioi 1)) z

Tactic:
(sbtw_iff_left_ne_and_right_mem_image_Ioi.1 h).2

Premises used: sbtw_iff_left_ne_and_right_mem_image_Ioi, And.right, Iff.mp
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
h : Sbtw R x y z
⊢ Membership.mem (γ := AffineSubspace R P) (affineSpan R {x, y}) z

Tactic:
h.wbtw.right_mem_affineSpan_of_left_ne h.left_ne

Premises used: Sbtw.wbtw, Wbtw.right_mem_affineSpan_of_left_ne, Sbtw.left_ne
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
rw :
  Wbtw R z y x ↔
    z = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ici 1)) x
rw₁ rw₂ :
  z = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ici 1)) x ↔
    z = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ici 1)) x
⊢ Wbtw R x y z ↔
    z = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap z y) : (a : R) → P) (Set.Ici 1)) x

Tactic:
rw [wbtw_comm, wbtw_iff_left_eq_or_right_mem_image_Ici]

Premises used: wbtw_comm, wbtw_iff_left_eq_or_right_mem_image_Ici