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
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
rw₃ 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)

Tactic:
rw [lineMap_apply, lineMap_apply, lineMap_vsub_left, smul_smul]

Premises used: AffineMap.lineMap_vsub_left, smul_smul, 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 : IsOrderedRing R
w x y z : P
h₁ : Wbtw R w x z
h₂ : Wbtw R x y z
rw : ∀ (h₁ : Wbtw R z x w) (h₂ : Wbtw R z y x), Wbtw R z y w
⊢ Wbtw R w y z

Tactic:
rw [wbtw_comm] at *

Premises used: wbtw_comm
-- 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 z x w
h₂ : Wbtw R z y x
⊢ Wbtw R z y w

Tactic:
h₁.trans_left h₂

Premises used: Wbtw.trans_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
w x y z : P
h₁ : Wbtw R z x w
h₂ : Wbtw R z y x
⊢ Wbtw R z y w

Tactic:
exact h₁.trans_left h₂

Premises used: Wbtw.trans_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
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

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

Premises used: Sbtw.left_ne_right, And.intro, Iff.intro, Sbtw.mem_image_Ioo
-- 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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
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
⊢ 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

Tactic:
refine ⟨fun h => ⟨h.mem_image_Ioo, h.left_ne_right⟩, 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
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
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
⊢ Sbtw R x y z

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

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
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

Tactic:
⟨⟨t, Set.mem_Icc_of_Ioo ht, rfl⟩, ?_⟩

Premises used: Set.mem_Icc_of_Ioo, And.intro, Exists.intro, Sbtw, 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
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
refine : (lineMap x z : (a : R) → P) t ≠ x ∧ (lineMap x z : (a : R) → P) t ≠ z
⊢ Sbtw R x ((lineMap x z : (a : R) → P) t) z

Tactic:
refine ⟨⟨t, Set.mem_Icc_of_Ioo ht, 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
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
rw : t • (z -ᵥ x) + 0 ≠ 0 ∧ (t - 1) • (z -ᵥ x) ≠ 0
⊢ (lineMap x z : (a : R) → P) t ≠ x ∧ (lineMap x z : (a : R) → P) t ≠ z

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]

Premises used: vadd_vsub_assoc, neg_one_smul, vsub_ne_zero, sub_eq_add_neg, AffineMap.lineMap_apply, add_smul, neg_vsub_eq_vsub_rev, vsub_self
-- 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
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
⊢ t • (z -ᵥ x) + 0 ≠ 0 ∧ (t - 1) • (z -ᵥ x) ≠ 0

Tactic:
simp [sub_eq_zero, ht.1.ne.symm, ht.2.ne, hxz.symm]

Premises used: sub_eq_zero, Ne.symm, And.right, And.left, LT.lt.ne
-- 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
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
mpr : x = y → Wbtw R x y z ∧ Wbtw R y x z
⊢ Wbtw R x y z ∧ Wbtw R y x z ↔ x = y

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

Tactic:
rcases hxyz with ⟨ty, hty, 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
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
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
⊢ x = (lineMap x z : (a : R) → P) ty

Tactic:
rcases hyxz with ⟨tx, htx, hx⟩
-- 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
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
⊢ (tx • (z -ᵥ (ty • (z -ᵥ x) +ᵥ x)) + ty • (z -ᵥ x)) +ᵥ x = x

Tactic:
rw [lineMap_apply, lineMap_apply, ← add_vadd] at hx

Premises used: AddSemigroupAction.add_vadd, 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 : 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 : (tx • (z -ᵥ (ty • (z -ᵥ x) +ᵥ x)) + ty • (z -ᵥ x)) +ᵥ x = x
⊢ tx - tx * ty + ty = 0 ∨ z -ᵥ x = 0

Tactic:
rw [← @vsub_eq_zero_iff_eq V, vadd_vsub, vsub_vadd_eq_vsub_sub, smul_sub, smul_smul, ← sub_smul,
      ← add_smul, smul_eq_zero] at hx

Premises used: vsub_vadd_eq_vsub_sub, vsub_eq_zero_iff_eq, sub_smul, smul_smul, smul_sub, add_smul, vadd_vsub, smul_eq_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
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 : tx - tx * ty + ty = 0 ∨ z -ᵥ x = 0
mp : ∀ (h : tx - tx * ty + ty = 0), x = (lineMap x z : (a : R) → P) ty
mp₁ : ∀ (h : z -ᵥ x = 0), x = (lineMap x z : (a : R) → P) ty
⊢ x = (lineMap x z : (a : R) → P) ty

Tactic:
rcases hx with (h | 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
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
h : tx - tx * ty + ty = 0
⊢ tx * 1 - tx * ty + ty = 0

Tactic:
nth_rw 1 [← mul_one tx] at h

Premises used: mul_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 : 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
h : tx * 1 - tx * ty + ty = 0
⊢ -(tx * (1 - ty)) = ty

Tactic:
rw [← mul_sub, add_eq_zero_iff_neg_eq] at h

Premises used: mul_sub, add_eq_zero_iff_neg_eq
-- 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
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
h : -(tx * (1 - ty)) = ty
⊢ ty = 0

Tactic:
le_antisymm ?_ hty.1

Premises used: le_antisymm, And.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
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
h : -(tx * (1 - ty)) = ty
refine : ty ≤ 0
⊢ ty = 0

Tactic:
refine le_antisymm ?_ hty.1

Premises used: le_antisymm, And.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
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
h : -(tx * (1 - ty)) = ty
rw : 0 ≤ tx * (1 - ty)
⊢ ty ≤ 0

Tactic:
rw [← h, Left.neg_nonpos_iff]

Premises used: Left.neg_nonpos_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
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
h : -(tx * (1 - ty)) = ty
⊢ 0 ≤ tx * (1 - ty)

Tactic:
mul_nonneg htx.1 (sub_nonneg.2 hty.2)

Premises used: Iff.mpr, mul_nonneg, And.right, And.left, sub_nonneg
-- 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
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
h : -(tx * (1 - ty)) = ty
⊢ 0 ≤ tx * (1 - ty)

Tactic:
exact mul_nonneg htx.1 (sub_nonneg.2 hty.2)

Premises used: Iff.mpr, mul_nonneg, And.right, And.left, sub_nonneg
-- 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
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
h : -(tx * (1 - ty)) = ty
⊢ ty = 0

Tactic:
have h' : ty = 0 := by
        refine le_antisymm ?_ hty.1
        rw [← h, Left.neg_nonpos_iff]
        exact mul_nonneg htx.1 (sub_nonneg.2 hty.2)
-- 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
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
h : -(tx * (1 - ty)) = ty
h' : ty = 0
⊢ x = (lineMap x z : (a : R) → P) ty

Tactic:
simp [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
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
h : z -ᵥ x = 0
⊢ z = x

Tactic:
rw [vsub_eq_zero_iff_eq] at h

Premises used: vsub_eq_zero_iff_eq
-- 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
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
h : z = x
mp : x = (lineMap x x : (a : R) → P) ty
mp₁ mp₂ : x = x
⊢ x = (lineMap x z : (a : R) → P) ty

Tactic:
rw [h, lineMap_same_apply]

Premises used: AffineMap.lineMap_same_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 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x z : P
⊢ Wbtw R x x z ∧ Wbtw R x x z

Tactic:
⟨wbtw_self_left _ _ _, wbtw_self_left _ _ _⟩

Premises used: wbtw_self_left, And.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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x z : P
⊢ Wbtw R x x z ∧ Wbtw R x x z

Tactic:
exact ⟨wbtw_self_left _ _ _, 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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
rw : Wbtw R z y x ∧ Wbtw R y z x ↔ z = y
⊢ Wbtw R x y z ∧ Wbtw R x z y ↔ y = z

Tactic:
rw [wbtw_comm, wbtw_comm (z := y), eq_comm]

Premises used: eq_comm, wbtw_comm
-- 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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
⊢ Wbtw R z y x ∧ Wbtw R y z x ↔ z = y

Tactic:
wbtw_swap_left_iff R x

Premises used: wbtw_swap_left_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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
⊢ Wbtw R z y x ∧ Wbtw R y z x ↔ z = y

Tactic:
exact wbtw_swap_left_iff R x

Premises used: wbtw_swap_left_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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
y z x : P
rw : Wbtw R z y x ∧ Wbtw R z x y ↔ x = y
rw₁ : y = x ↔ x = y
rw₂ rw₃ : x = y ↔ x = y
⊢ Wbtw R x y z ∧ Wbtw R z x y ↔ x = y

Tactic:
rw [wbtw_comm, wbtw_swap_right_iff, eq_comm]

Premises used: wbtw_swap_right_iff, eq_comm, wbtw_comm
-- 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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
h : Wbtw R x y z
rw : Wbtw R y x z ↔ Wbtw R x y z ∧ Wbtw R y x z
rw₁ rw₂ : Wbtw R y x z ↔ Wbtw R y x z
⊢ Wbtw R y x z ↔ x = y

Tactic:
rw [← wbtw_swap_left_iff R z, and_iff_right h]

Premises used: and_iff_right, wbtw_swap_left_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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
h : Wbtw R x y z
rw : Wbtw R x z y ↔ Wbtw R x y z ∧ Wbtw R x z y
rw₁ rw₂ : Wbtw R x z y ↔ Wbtw R x z y
⊢ Wbtw R x z y ↔ y = z

Tactic:
rw [← wbtw_swap_right_iff R x, and_iff_right h]

Premises used: wbtw_swap_right_iff, and_iff_right
-- 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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
h : Wbtw R x y z
rw : Wbtw R z x y ↔ Wbtw R x y z ∧ Wbtw R z x y
rw₁ : P
rw₂ rw₃ : Wbtw R z x y ↔ Wbtw R z x y
⊢ Wbtw R z x y ↔ x = y

Tactic:
rw [← wbtw_rotate_iff R x, and_iff_right h]

Premises used: and_iff_right, wbtw_rotate_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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
h : Sbtw R x y z
⊢ ¬Wbtw R y x z

Tactic:
fun hs =>
  h.left_ne (h.wbtw.swap_left_iff.1 hs)

Premises used: Wbtw.swap_left_iff, Sbtw.wbtw, Iff.mp, Not, Sbtw.left_ne
-- 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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
h : Sbtw R x y z
⊢ ¬Wbtw R x z y

Tactic:
fun hs =>
  h.ne_right (h.wbtw.swap_right_iff.1 hs)

Premises used: Wbtw.swap_right_iff, Sbtw.wbtw, Iff.mp, Sbtw.ne_right, Not
-- 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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
h : Sbtw R x y z
⊢ ¬Wbtw R z x y

Tactic:
fun hs =>
  h.left_ne (h.wbtw.rotate_iff.1 hs)

Premises used: Sbtw.wbtw, Iff.mp, Wbtw.rotate_iff, Not, Sbtw.left_ne
-- 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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y : P
r : R
pos : ∀ (hxy : x = y), Wbtw R x ((lineMap x y : (a : R) → P) r) y ↔ x = y ∨ Membership.mem (γ := Set R) (Set.Icc 0 1) r
neg : ∀ (hxy : ¬x = y), Wbtw R x ((lineMap x y : (a : R) → P) r) y ↔ x = y ∨ Membership.mem (γ := Set R) (Set.Icc 0 1) r
⊢ Wbtw R x ((lineMap x y : (a : R) → P) r) y ↔ x = y ∨ Membership.mem (γ := Set R) (Set.Icc 0 1) r

Tactic:
by_cases hxy : x = y
-- 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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y : P
r : R
hxy : x = y
pos : Wbtw R y y y ↔ y = y ∨ Membership.mem (γ := Set R) (Set.Icc 0 1) r
⊢ Wbtw R x ((lineMap x y : (a : R) → P) r) y ↔ x = y ∨ Membership.mem (γ := Set R) (Set.Icc 0 1) r

Tactic:
rw [hxy, lineMap_same_apply]

Premises used: AffineMap.lineMap_same_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 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y : P
r : R
hxy : x = y
⊢ Wbtw R y y y ↔ y = y ∨ Membership.mem (γ := Set R) (Set.Icc 0 1) r

Tactic:
simp
-- 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
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y : P
r : R
hxy : ¬x = y
neg : Wbtw R x ((lineMap x y : (a : R) → P) r) y ↔ Membership.mem (γ := Set R) (Set.Icc 0 1) r
neg₁ :
  Membership.mem (α := P) (affineSegment R x y) ((lineMap x y : (a : R) → P) r : P) ↔
    Membership.mem (γ := Set R) (Set.Icc 0 1) r
neg₂ :
  Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Icc 0 1)) ((lineMap x y : (a : R) → P) r : P) ↔
    Membership.mem (γ := Set R) (Set.Icc 0 1) r
neg₃ neg₄ : Membership.mem (γ := Set R) (Set.Icc 0 1) r ↔ Membership.mem (γ := Set R) (Set.Icc 0 1) r
⊢ Wbtw R x ((lineMap x y : (a : R) → P) r) y ↔ x = y ∨ Membership.mem (γ := Set R) (Set.Icc 0 1) r

Tactic:
rw [or_iff_right hxy, Wbtw, affineSegment, (lineMap_injective R hxy).mem_set_image]

Premises used: affineSegment, AffineMap.lineMap_injective, Wbtw, or_iff_right, Function.Injective.mem_set_image