awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : IsOrderedRing R
p₀ p₁ p₂ : V
s : Set V
hs : Convex R s
h₀₁₂ : Wbtw R p₀ p₁ p₂
h₀ : p₀ ∈ s
h₂ : p₂ ∈ s
⊢ p₁ ∈ s

Tactic:
hs.segment_subset h₀ h₂ h₀₁₂.mem_segment

Premises used: Convex.segment_subset, Wbtw.mem_segment
-- 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
rw : y ∈ affineSegment R x z ↔ Wbtw R z y x
rw₁ : y ∈ affineSegment R x z ↔ y ∈ affineSegment R z x
rw₂ rw₃ : y ∈ affineSegment R z x ↔ y ∈ affineSegment R z x
⊢ Wbtw R x y z ↔ Wbtw R z y x

Tactic:
rw [Wbtw, Wbtw, affineSegment_comm]

Premises used: affineSegment_comm, 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 z : P
rw : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Sbtw R z y x
rw₁ : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R z y x ∧ y ≠ z ∧ y ≠ x
rw₂ : Wbtw R z y x ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R z y x ∧ y ≠ z ∧ y ≠ x
rw₃ : (Wbtw R z y x ∧ y ≠ x) ∧ y ≠ z ↔ Wbtw R z y x ∧ y ≠ z ∧ y ≠ x
rw₄ : (Wbtw R z y x ∧ y ≠ x) ∧ y ≠ z ↔ (Wbtw R z y x ∧ y ≠ z) ∧ y ≠ x
rw₅ rw₆ : (Wbtw R z y x ∧ y ≠ z) ∧ y ≠ x ↔ (Wbtw R z y x ∧ y ≠ z) ∧ y ≠ x
⊢ Sbtw R x y z ↔ Sbtw R z y x

Tactic:
rw [Sbtw, Sbtw, wbtw_comm, ← and_assoc, ← and_assoc, and_right_comm]

Premises used: wbtw_comm, and_assoc, and_right_comm, 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
s : AffineSubspace R P
x y z : P
hxyz : Wbtw R x y z
hx : x ∈ s
hz : z ∈ s
obtain : ∀ (ε : R), Membership.mem (α := P) s ((lineMap x z : (a : R) → P) ε : P)
⊢ y ∈ s

Tactic:
obtain ⟨ε, -, rfl⟩ := hxyz

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
s : AffineSubspace R P
x z : P
hx : x ∈ s
hz : z ∈ s
ε : R
⊢ Membership.mem (α := P) s ((lineMap x z : (a : R) → P) ε : P)

Tactic:
lineMap_mem _ hx hz

Premises used: AffineMap.lineMap_mem
-- 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
s : AffineSubspace R P
x z : P
hx : x ∈ s
hz : z ∈ s
ε : R
⊢ Membership.mem (α := P) s ((lineMap x z : (a : R) → P) ε : P)

Tactic:
exact lineMap_mem _ hx hz

Premises used: AffineMap.lineMap_mem
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
h : Wbtw R x y z
f : P →ᵃ[R] P'
rw :
  Membership.mem.{u_5, u_5} (α := P') (γ := Set P') ((⇑f : (a : P) → P') '' affineSegment R x z)
    ((f : (a : P) → P') y : P')
⊢ Wbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P')

Tactic:
rw [Wbtw, ← affineSegment_image]

Premises used: Wbtw, affineSegment_image
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
h : Wbtw R x y z
f : P →ᵃ[R] P'
⊢ Membership.mem.{u_5, u_5} (α := P') (γ := Set P') ((⇑f : (a : P) → P') '' affineSegment R x z)
    ((f : (a : P) → P') y : P')

Tactic:
Set.mem_image_of_mem _ h

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
h : Wbtw R x y z
f : P →ᵃ[R] P'
⊢ Membership.mem.{u_5, u_5} (α := P') (γ := Set P') ((⇑f : (a : P) → P') '' affineSegment R x z)
    ((f : (a : P) → P') y : P')

Tactic:
exact Set.mem_image_of_mem _ h

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
hf : Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
⊢ Wbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P') ↔
    Wbtw R x y z

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

Premises used: Wbtw.map, Iff.intro
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
hf : Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
refine :
  ∀
    (h :
      Wbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P')
        ((f : (a : P) → P') z : P')),
    Wbtw R x y z
⊢ Wbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P') ↔
    Wbtw R x y z

Tactic:
refine ⟨fun h => ?_, fun h => h.map _⟩
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
hf : Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
h : Wbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P')
rwa :
  ∀
    (h :
      Membership.mem.{u_5, u_5} (α := P') (γ := Set P')
        (affineSegment R ((f : (a : P) → P') x) ((f : (a : P) → P') z) : Set P') ((f : (a : P) → P') y : P')),
    Wbtw R x y z
rwa₁ :
  ∀
    (h :
      Membership.mem.{u_5, u_5} (α := P') (γ := Set P') ((⇑f : (a : P) → P') '' affineSegment R x z)
        ((f : (a : P) → P') y : P')),
    Wbtw R x y z
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : y ∈ affineSegment R x z), Wbtw R x y z
⊢ Wbtw R x y z

Tactic:
rwa [Wbtw, ← affineSegment_image, hf.mem_set_image] at h

Premises used: Wbtw, affineSegment_image, Function.Injective.mem_set_image
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
hf : Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑f : (a : P) → P')
simp_rw :
  Wbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P') ∧
      Ne.{u_5 + 1} (α := P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') x : P') ∧
        Ne.{u_5 + 1} (α := P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P') ↔
    Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
simp_rw₁ :
  Wbtw R x y z ∧
      Ne.{u_5 + 1} (α := P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') x : P') ∧
        Ne.{u_5 + 1} (α := P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P') ↔
    Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
⊢ Sbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P') ↔
    Sbtw R x y z

Tactic:
simp_rw [Sbtw, hf.wbtw_map_iff, hf.ne_iff]

Premises used: Function.Injective.ne_iff, Function.Injective.wbtw_map_iff, Sbtw
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
s : AffineSubspace R P
hf : InjOn.{u_4, u_5} (β := P') (⇑f : (a : P) → P') (↑s : Set P)
hx : x ∈ s
hy : y ∈ s
hz : z ∈ s
⊢ Wbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P') ↔
    Wbtw R x y z

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

Premises used: Wbtw.map, Iff.intro
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
s : AffineSubspace R P
hf : InjOn.{u_4, u_5} (β := P') (⇑f : (a : P) → P') (↑s : Set P)
hx : x ∈ s
hy : y ∈ s
hz : z ∈ s
refine :
  ∀
    (h :
      Wbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P')
        ((f : (a : P) → P') z : P')),
    Wbtw R x y z
⊢ Wbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P') ↔
    Wbtw R x y z

Tactic:
refine ⟨fun h => ?_, fun h => h.map _⟩
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
s : AffineSubspace R P
hf : InjOn.{u_4, u_5} (β := P') (⇑f : (a : P) → P') (↑s : Set P)
hx : x ∈ s
hy : y ∈ s
hz : z ∈ s
h : Wbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P')
rwa :
  ∀
    (h :
      Membership.mem.{u_5, u_5} (α := P') (γ := Set P')
        (affineSegment R ((f : (a : P) → P') x) ((f : (a : P) → P') z) : Set P') ((f : (a : P) → P') y : P')),
    Wbtw R x y z
rwa₁ :
  ∀
    (h :
      Membership.mem.{u_5, u_5} (α := P') (γ := Set P') ((⇑f : (a : P) → P') '' affineSegment R x z)
        ((f : (a : P) → P') y : P')),
    Wbtw R x y z
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : y ∈ affineSegment R x z), Wbtw R x y z
⊢ Wbtw R x y z

Tactic:
rwa [Wbtw, ← affineSegment_image, hf.mem_image_iff
    ((affineSegment_subset_affineSpan R x z).trans (affineSpan_le.2 (Set.pair_subset hx hz))) hy]
    at h

Premises used: Iff.mpr, Set.pair_subset, Wbtw, HasSubset.Subset.trans, affineSpan_le, Set.InjOn.mem_image_iff, affineSegment_subset_affineSpan, affineSegment_image
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
s : AffineSubspace R P
hf : InjOn.{u_4, u_5} (β := P') (⇑f : (a : P) → P') (↑s : Set P)
hx : x ∈ s
hy : y ∈ s
hz : z ∈ s
simp_rw :
  Wbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P') ∧
      Ne.{u_5 + 1} (α := P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') x : P') ∧
        Ne.{u_5 + 1} (α := P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P') ↔
    Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
simp_rw₁ :
  Wbtw R x y z ∧
      Ne.{u_5 + 1} (α := P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') x : P') ∧
        Ne.{u_5 + 1} (α := P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P') ↔
    Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
simp_rw₂ :
  Wbtw R x y z ∧ y ≠ x ∧ Ne.{u_5 + 1} (α := P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P') ↔
    Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
⊢ Sbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P') ↔
    Sbtw R x y z

Tactic:
simp_rw [Sbtw, hf.wbtw_map_iff hx hy hz, hf.ne_iff hy hx, hf.ne_iff hy hz]

Premises used: Set.InjOn.wbtw_map_iff, Set.InjOn.ne_iff, Sbtw
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
f : P ≃ᵃ[R] P'
⊢ Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑(↑f : P →ᵃ[R] P') : (a : P) → P')

Tactic:
have : Function.Injective f.toAffineMap := f.injective
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
f : P ≃ᵃ[R] P'
this : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑(↑f : P →ᵃ[R] P') : (a : P) → P')
⊢ Wbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P') ↔
    Wbtw R x y z

Tactic:
apply this.wbtw_map_iff

Premises used: Function.Injective.wbtw_map_iff
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
x y z : P
f : P ≃ᵃ[R] P'
this : Function.Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P') (⇑(↑f : P →ᵃ[R] P') : (a : P) → P')
⊢ Sbtw.{u_1, u_3, u_5} R (P := P') ((f : (a : P) → P') x : P') ((f : (a : P) → P') y : P') ((f : (a : P) → P') z : P') ↔
    Sbtw R x y z

Tactic:
apply this.sbtw_map_iff

Premises used: Function.Injective.sbtw_map_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
x y z : P
v : V
⊢ Wbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Wbtw R x y z

Tactic:
mem_const_vadd_affineSegment _

Premises used: mem_const_vadd_affineSegment, Wbtw
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
x y z v : V
⊢ Wbtw R (v + x) (v + y) (v + z) ↔ Wbtw R x y z

Tactic:
wbtw_const_vadd_iff v

Premises used: wbtw_const_vadd_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
x y z : V
p : P
⊢ Wbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Wbtw R x y z

Tactic:
mem_vadd_const_affineSegment _

Premises used: Wbtw, mem_vadd_const_affineSegment
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
x y z v : V
⊢ Wbtw R (x + v) (y + v) (z + v) ↔ Wbtw R x y z

Tactic:
wbtw_vadd_const_iff v

Premises used: wbtw_vadd_const_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
x y z p : P
⊢ Wbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Wbtw R x y z

Tactic:
mem_const_vsub_affineSegment _

Premises used: Wbtw, mem_const_vsub_affineSegment
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
x y z v : V
⊢ Wbtw R (v - x) (v - y) (v - z) ↔ Wbtw R x y z

Tactic:
wbtw_const_vsub_iff v

Premises used: wbtw_const_vsub_iff
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
x y z : V
⊢ Wbtw R (-x) (-y) (-z) ↔ Wbtw R x y z

Tactic:
simp only [← zero_sub, wbtw_const_sub_iff]

Premises used: wbtw_const_sub_iff, zero_sub
-- 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 : P
⊢ Wbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Wbtw R x y z

Tactic:
mem_vsub_const_affineSegment _

Premises used: Wbtw, mem_vsub_const_affineSegment
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
x y z v : V
⊢ Wbtw R (x - v) (y - v) (z - v) ↔ Wbtw R x y z

Tactic:
wbtw_vsub_const_iff v

Premises used: wbtw_vsub_const_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
x y z : P
v : V
rw : Wbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ∧ v +ᵥ y ≠ v +ᵥ x ∧ v +ᵥ y ≠ v +ᵥ z ↔ Sbtw R x y z
rw₁ : Wbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ∧ v +ᵥ y ≠ v +ᵥ x ∧ v +ᵥ y ≠ v +ᵥ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
rw₂ : Wbtw R x y z ∧ v +ᵥ y ≠ v +ᵥ x ∧ v +ᵥ y ≠ v +ᵥ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
rw₃ : Wbtw R x y z ∧ y ≠ x ∧ v +ᵥ y ≠ v +ᵥ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
rw₄ rw₅ : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
⊢ Sbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Sbtw R x y z

Tactic:
rw [Sbtw, Sbtw, wbtw_const_vadd_iff, (AddAction.injective v).ne_iff,
    (AddAction.injective v).ne_iff]

Premises used: Function.Injective.ne_iff, AddAction.injective, wbtw_const_vadd_iff, Sbtw
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
x y z v : V
⊢ Sbtw R (v + x) (v + y) (v + z) ↔ Sbtw R x y z

Tactic:
sbtw_const_vadd_iff v

Premises used: sbtw_const_vadd_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
x y z : V
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
rw₄ rw₅ : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
⊢ Sbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Sbtw R x y z

Tactic:
rw [Sbtw, Sbtw, wbtw_vadd_const_iff, (vadd_right_injective p).ne_iff,
    (vadd_right_injective p).ne_iff]

Premises used: Function.Injective.ne_iff, vadd_right_injective, wbtw_vadd_const_iff, Sbtw
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
x y z v : V
⊢ Sbtw R (x + v) (y + v) (z + v) ↔ Sbtw R x y z

Tactic:
sbtw_vadd_const_iff v

Premises used: sbtw_vadd_const_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
x y z p : P
rw : Wbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ∧ p -ᵥ y ≠ p -ᵥ x ∧ p -ᵥ y ≠ p -ᵥ z ↔ Sbtw R x y z
rw₁ : Wbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ∧ p -ᵥ y ≠ p -ᵥ x ∧ p -ᵥ y ≠ p -ᵥ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
rw₂ : Wbtw R x y z ∧ p -ᵥ y ≠ p -ᵥ x ∧ p -ᵥ y ≠ p -ᵥ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
rw₃ : Wbtw R x y z ∧ y ≠ x ∧ p -ᵥ y ≠ p -ᵥ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
rw₄ rw₅ : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
⊢ Sbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Sbtw R x y z

Tactic:
rw [Sbtw, Sbtw, wbtw_const_vsub_iff, (vsub_right_injective p).ne_iff,
    (vsub_right_injective p).ne_iff]

Premises used: wbtw_const_vsub_iff, vsub_right_injective, Function.Injective.ne_iff, Sbtw
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
x y z v : V
⊢ Sbtw R (v - x) (v - y) (v - z) ↔ Sbtw R x y z

Tactic:
sbtw_const_vsub_iff v

Premises used: sbtw_const_vsub_iff
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
x y z : V
⊢ Sbtw R (-x) (-y) (-z) ↔ Sbtw R x y z

Tactic:
simp only [← zero_sub, sbtw_const_sub_iff]

Premises used: sbtw_const_sub_iff, zero_sub
-- 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 : 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
rw₄ rw₅ : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
⊢ Sbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Sbtw R x y z

Tactic:
rw [Sbtw, Sbtw, wbtw_vsub_const_iff, (vsub_left_injective p).ne_iff,
    (vsub_left_injective p).ne_iff]

Premises used: Function.Injective.ne_iff, vsub_left_injective, wbtw_vsub_const_iff, Sbtw
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
x y z v : V
⊢ Sbtw R (x - v) (y - v) (z - v) ↔ Sbtw R x y z

Tactic:
sbtw_vsub_const_iff v

Premises used: sbtw_vsub_const_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
x y z : P
h : Sbtw R x y z
⊢ Wbtw R x y z

Tactic:
h.1

Premises used: 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
x y z : P
h : Sbtw R x y z
⊢ y ≠ x

Tactic:
h.2.1

Premises used: And.right, 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
x y z : P
h : Sbtw R x y z
⊢ x ≠ y

Tactic:
h.2.1.symm

Premises used: Ne.symm, And.right, 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
x y z : P
h : Sbtw R x y z
⊢ y ≠ z

Tactic:
h.2.2

Premises used: And.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
x y z : P
h : Sbtw R x y z
⊢ z ≠ y

Tactic:
h.2.2.symm

Premises used: Ne.symm, And.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
x y z : P
h : Sbtw R x y z
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)
⊢ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x z) : (a : R) → P) (Set.Ioo 0 1)) y

Tactic:
rcases h with ⟨⟨t, ht, rfl⟩, hyx, hyz⟩

Premises used: rfl