awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Between
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)
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)
⊢ 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)

Premises used: Set.eq_endpoints_or_mem_Ioo_of_mem_Icc, rfl
-- Module: Mathlib.Analysis.Convex.Between
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
inl : False
⊢ 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:
exfalso
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ False

Tactic:
hyx (lineMap_apply_zero _ _)

Premises used: AffineMap.lineMap_apply_zero
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ False

Tactic:
exact hyx (lineMap_apply_zero _ _)

Premises used: AffineMap.lineMap_apply_zero
-- Module: Mathlib.Analysis.Convex.Between
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
inr : False
⊢ 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:
exfalso
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ False

Tactic:
hyz (lineMap_apply_one _ _)

Premises used: AffineMap.lineMap_apply_one
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ False

Tactic:
exact hyz (lineMap_apply_one _ _)

Premises used: AffineMap.lineMap_apply_one
-- Module: Mathlib.Analysis.Convex.Between
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
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:
⟨t, ho, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Analysis.Convex.Between
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
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:
exact ⟨t, ho, rfl⟩
-- Module: Mathlib.Analysis.Convex.Between
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
rcases :
  ∀ (r : R), Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R {x, z}) ((lineMap x z : (a : R) → P) r : P)
⊢ Membership.mem (γ := AffineSubspace R P) (affineSpan R {x, z}) y

Tactic:
rcases h with ⟨r, ⟨-, rfl⟩⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Between
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
r : R
⊢ Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R {x, z}) ((lineMap x z : (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 : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x z : P
r : R
⊢ Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R {x, z}) ((lineMap x z : (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 : 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 x y

Tactic:
left_mem_affineSegment _ _ _

Premises used: Wbtw, left_mem_affineSegment
-- Module: Mathlib.Analysis.Convex.Between
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 y

Tactic:
right_mem_affineSegment _ _ _

Premises used: Wbtw, right_mem_affineSegment
-- Module: Mathlib.Analysis.Convex.Between
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

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 : 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
refine_2 : ∀ (h : y = x), Wbtw R x y x
⊢ Wbtw R x y x ↔ y = x

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 : 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
⊢ y = x

Tactic:
simpa [Wbtw, affineSegment] using h

Premises used: affineSegment, Wbtw
-- Module: Mathlib.Analysis.Convex.Between
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
refine_2 : Wbtw R x x x
⊢ Wbtw R x y x

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Convex.Between
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 x x

Tactic:
wbtw_self_left R x x

Premises used: wbtw_self_left
-- Module: Mathlib.Analysis.Convex.Between
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 x x

Tactic:
exact wbtw_self_left R x x

Premises used: wbtw_self_left
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ Eq.{u_4 + 1} (α := P) ((lineMap x y : (a : R) → P) (HSMul.hSMul (β := R) a 1) : P)
    ((lineMap x y : (a : R') → P) a : P)

Tactic:
simp [lineMap_apply]

Premises used: AffineMap.lineMap_apply
-- Module: Mathlib.Analysis.Convex.Between
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
refine_2 : HSMul.hSMul (β := R) a 1 ≤ 1
⊢ Membership.mem (α := P) (affineSegment R x y) ((lineMap x y : (a : R') → P) a : P)

Tactic:
refine ⟨a • 1, ⟨?_, ?_⟩, by simp [lineMap_apply]⟩
-- Module: Mathlib.Analysis.Convex.Between
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 : HSMul.hSMul.{u_6, u_1, u_1} (α := R') (β := R) 0 1 ≤ HSMul.hSMul (β := R) a 1
⊢ 0 ≤ HSMul.hSMul (β := R) a 1

Tactic:
rw [← zero_smul R' (1 : R)]

Premises used: zero_smul, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Between
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.{u_6, u_1, u_1} (α := R') (β := R) 0 1 ≤ HSMul.hSMul (β := R) a 1

Tactic:
smul_le_smul_of_nonneg_right ha₀ zero_le_one

Premises used: smul_le_smul_of_nonneg_right, zero_le_one
-- Module: Mathlib.Analysis.Convex.Between
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.{u_6, u_1, u_1} (α := R') (β := R) 0 1 ≤ HSMul.hSMul (β := R) a 1

Tactic:
exact smul_le_smul_of_nonneg_right ha₀ zero_le_one

Premises used: smul_le_smul_of_nonneg_right, zero_le_one
-- Module: Mathlib.Analysis.Convex.Between
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_2 : HSMul.hSMul (β := R) a 1 ≤ HSMul.hSMul.{u_6, u_1, u_1} (α := R') (β := R) 1 1
⊢ HSMul.hSMul (β := R) a 1 ≤ 1

Tactic:
nth_rw 2 [← one_smul R' 1]

Premises used: one_smul, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Between
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 ≤ HSMul.hSMul.{u_6, u_1, u_1} (α := R') (β := R) 1 1

Tactic:
smul_le_smul_of_nonneg_right ha₁ zero_le_one

Premises used: smul_le_smul_of_nonneg_right, zero_le_one
-- Module: Mathlib.Analysis.Convex.Between
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 ≤ HSMul.hSMul.{u_6, u_1, u_1} (α := R') (β := R) 1 1

Tactic:
exact smul_le_smul_of_nonneg_right ha₁ zero_le_one

Premises used: smul_le_smul_of_nonneg_right, zero_le_one
-- Module: Mathlib.Analysis.Convex.Between
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 z : P
h : Wbtw R' x y z
⊢ Wbtw R x y z

Tactic:
affineSegment.lift R R' x z h

Premises used: Wbtw, affineSegment.lift
-- Module: Mathlib.Analysis.Convex.Between
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 z : P
h : Sbtw R' x y z
⊢ Sbtw R x y z

Tactic:
⟨h.wbtw.lift R, h.2⟩

Premises used: And.right, And.intro, Sbtw.wbtw, Wbtw.lift, Sbtw
-- Module: Mathlib.Analysis.Convex.Between
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 : P
⊢ ¬Sbtw R x x y

Tactic:
fun h => h.ne_left rfl

Premises used: Sbtw.ne_left, Not, rfl
-- Module: Mathlib.Analysis.Convex.Between
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 : P
⊢ ¬Sbtw R x y y

Tactic:
fun h => h.ne_right rfl

Premises used: Sbtw.ne_right, Not, rfl
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ y = x

Tactic:
rw [wbtw_self_iff] at h

Premises used: wbtw_self_iff
-- Module: Mathlib.Analysis.Convex.Between
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 : y = x
⊢ False

Tactic:
hne h
-- Module: Mathlib.Analysis.Convex.Between
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 : y = x
⊢ False

Tactic:
exact hne h
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ y = x

Tactic:
rw [wbtw_self_iff] at h

Premises used: wbtw_self_iff
-- Module: Mathlib.Analysis.Convex.Between
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
h₁ : y = x
⊢ y ≠ x

Tactic:
rw [wbtw_self_iff] at h

Premises used: wbtw_self_iff
-- Module: Mathlib.Analysis.Convex.Between
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
hne : y ≠ x
⊢ False

Tactic:
hne h
-- Module: Mathlib.Analysis.Convex.Between
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
hne : y ≠ x
⊢ False

Tactic:
exact hne h
-- Module: Mathlib.Analysis.Convex.Between
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
h : Sbtw R x y z
⊢ x ≠ z

Tactic:
h.wbtw.left_ne_right_of_ne_left h.2.1

Premises used: Wbtw.left_ne_right_of_ne_left, And.right, And.left, Sbtw.wbtw
-- Module: Mathlib.Analysis.Convex.Between
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
⊢ ¬Sbtw R x y x

Tactic:
fun h => h.left_ne_right rfl

Premises used: Sbtw.left_ne_right, Not, rfl
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
x : R
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
⊢ (∃ (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

Tactic:
simp_rw [lineMap_apply_ring]

Premises used: AffineMap.lineMap_apply_ring
-- Module: Mathlib.Analysis.Convex.Between
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 ∧ (1 - x_1) * 0 + x_1 * 1 = x) ↔
    Membership.mem (γ := Set R) (Set.Icc 0 1) x

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Between
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
rw₁ rw₂ : Membership.mem (γ := Set R) (Set.Icc 0 1) x ↔ Membership.mem (γ := Set R) (Set.Icc 0 1) x
⊢ Wbtw R 1 x 0 ↔ Membership.mem (γ := Set R) (Set.Icc 0 1) x

Tactic:
rw [wbtw_comm, wbtw_zero_one_iff]

Premises used: wbtw_zero_one_iff, wbtw_comm
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
x : R
rw : (0 ≤ x ∧ x ≤ 1) ∧ x ≠ 0 ∧ x ≠ 1 ↔ 0 < x ∧ x < 1
⊢ Sbtw R 0 x 1 ↔ Membership.mem (γ := Set R) (Set.Ioo 0 1) x

Tactic:
rw [Sbtw, wbtw_zero_one_iff, Set.mem_Icc, Set.mem_Ioo]

Premises used: Set.mem_Ioo, wbtw_zero_one_iff, Set.mem_Icc, Sbtw
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
x : R
⊢ (0 ≤ x ∧ x ≤ 1) ∧ x ≠ 0 ∧ x ≠ 1 ↔ 0 < x ∧ x < 1

Tactic:
⟨fun h => ⟨h.1.1.lt_of_ne (Ne.symm h.2.1), h.1.2.lt_of_ne h.2.2⟩, fun h =>
      ⟨⟨h.1.le, h.2.le⟩, h.1.ne', h.2.ne⟩⟩

Premises used: LT.lt.le, Ne.symm, LE.le.lt_of_ne, LT.lt.ne', And.right, And.left, And.intro, Iff.intro, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
x : R
⊢ (0 ≤ x ∧ x ≤ 1) ∧ x ≠ 0 ∧ x ≠ 1 ↔ 0 < x ∧ x < 1

Tactic:
exact
    ⟨fun h => ⟨h.1.1.lt_of_ne (Ne.symm h.2.1), h.1.2.lt_of_ne h.2.2⟩, fun h =>
      ⟨⟨h.1.le, h.2.le⟩, h.1.ne', h.2.ne⟩⟩
-- Module: Mathlib.Analysis.Convex.Between
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
rw₁ rw₂ : Membership.mem (γ := Set R) (Set.Ioo 0 1) x ↔ Membership.mem (γ := Set R) (Set.Ioo 0 1) x
⊢ Sbtw R 1 x 0 ↔ Membership.mem (γ := Set R) (Set.Ioo 0 1) x

Tactic:
rw [sbtw_comm, sbtw_zero_one_iff]

Premises used: sbtw_comm, sbtw_zero_one_iff
-- Module: Mathlib.Analysis.Convex.Between
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
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
⊢ Wbtw R w x z

Tactic:
rcases h₁ with ⟨t₁, ht₁, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Between
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₁)
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
⊢ Wbtw R w x z

Tactic:
rcases h₂ with ⟨t₂, ht₂, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Between
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

Tactic:
⟨t₂ * t₁, ⟨mul_nonneg ht₂.1 ht₁.1, mul_le_one₀ ht₂.2 ht₁.1 ht₁.2⟩, ?_⟩

Premises used: affineSegment, mul_nonneg, HMul.hMul, Set.Mem, Wbtw, setOf, And.right, And.left, mul_le_one₀, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Analysis.Convex.Between
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₂
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)
⊢ Wbtw R w ((lineMap w ((lineMap w z : (a : R) → P) t₁) : (a : R) → P) t₂) z

Tactic:
refine ⟨t₂ * t₁, ⟨mul_nonneg ht₂.1 ht₁.1, mul_le_one₀ ht₂.2 ht₁.1 ht₁.2⟩, ?_⟩