awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
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')
⊢ 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
have 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
Tactic: simp_rw [Sbtw, hf.wbtw_map_iff, hf.ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
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
⊢ 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
have 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
Tactic: simp_rw [Sbtw, hf.wbtw_map_iff, hf.ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
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
have 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
Tactic: refine ⟨fun h => ?_, fun h => h.map _⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
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')
⊢ Wbtw R x y z
have 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
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
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
⊢ Wbtw R x y z
have 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
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
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
⊢ Wbtw R x y z
have rwa₂ : ∀ (h : y ∈ affineSegment R x 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
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
⊢ 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
have 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
Tactic: simp_rw [Sbtw, hf.wbtw_map_iff hx hy hz, hf.ne_iff hy hx, hf.ne_iff hy hz]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
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
⊢ 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
have 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
Tactic: simp_rw [Sbtw, hf.wbtw_map_iff hx hy hz, hf.ne_iff hy hx, hf.ne_iff hy hz]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
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
⊢ 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
have 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
Tactic: simp_rw [Sbtw, hf.wbtw_map_iff hx hy hz, hf.ne_iff hy hx, hf.ne_iff hy hz]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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'
⊢ 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
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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'
⊢ 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
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z : P
v : V
⊢ Sbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Sbtw R x y z
have rw : Wbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ∧ v +ᵥ y ≠ 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z : P
v : V
rw : Wbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ∧ v +ᵥ y ≠ v +ᵥ x ∧ v +ᵥ y ≠ v +ᵥ z ↔ Sbtw R x y z
⊢ Sbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Sbtw R x y z
have 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
Tactic: rw [Sbtw, Sbtw, wbtw_const_vadd_iff, (AddAction.injective v).ne_iff,
    (AddAction.injective v).ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z : P
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
⊢ Sbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Sbtw R x y z
have rw₂ : Wbtw R x y z ∧ v +ᵥ y ≠ v +ᵥ x ∧ v +ᵥ y ≠ v +ᵥ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Tactic: rw [Sbtw, Sbtw, wbtw_const_vadd_iff, (AddAction.injective v).ne_iff,
    (AddAction.injective v).ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z : P
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
⊢ Sbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Sbtw R x y z
have rw₃ : Wbtw R x y z ∧ y ≠ x ∧ v +ᵥ y ≠ v +ᵥ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Tactic: rw [Sbtw, Sbtw, wbtw_const_vadd_iff, (AddAction.injective v).ne_iff,
    (AddAction.injective v).ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z : P
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
⊢ Sbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Sbtw R x y z
have rw₄ : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Tactic: rw [Sbtw, Sbtw, wbtw_const_vadd_iff, (AddAction.injective v).ne_iff,
    (AddAction.injective v).ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z : V
p : P
⊢ Sbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Sbtw R x y z
have rw : Wbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ∧ y +ᵥ p ≠ 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z : 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
⊢ Sbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Sbtw R x y z
have 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
Tactic: rw [Sbtw, Sbtw, wbtw_vadd_const_iff, (vadd_right_injective p).ne_iff,
    (vadd_right_injective p).ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z : 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
⊢ Sbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Sbtw R x y z
have rw₂ : Wbtw R x y z ∧ y +ᵥ p ≠ x +ᵥ p ∧ y +ᵥ p ≠ z +ᵥ p ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Tactic: rw [Sbtw, Sbtw, wbtw_vadd_const_iff, (vadd_right_injective p).ne_iff,
    (vadd_right_injective p).ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z : 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
⊢ Sbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Sbtw R x y z
have rw₃ : Wbtw R x y z ∧ y ≠ x ∧ y +ᵥ p ≠ z +ᵥ p ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Tactic: rw [Sbtw, Sbtw, wbtw_vadd_const_iff, (vadd_right_injective p).ne_iff,
    (vadd_right_injective p).ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z : 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
⊢ Sbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Sbtw R x y z
have rw₄ : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Tactic: rw [Sbtw, Sbtw, wbtw_vadd_const_iff, (vadd_right_injective p).ne_iff,
    (vadd_right_injective p).ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z p : P
⊢ Sbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Sbtw R x y z
have rw : Wbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ∧ p -ᵥ y ≠ 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z p : P
rw : Wbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ∧ p -ᵥ y ≠ p -ᵥ x ∧ p -ᵥ y ≠ p -ᵥ z ↔ Sbtw R x y z
⊢ Sbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Sbtw R x y z
have 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
Tactic: rw [Sbtw, Sbtw, wbtw_const_vsub_iff, (vsub_right_injective p).ne_iff,
    (vsub_right_injective p).ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z p : 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
⊢ Sbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Sbtw R x y z
have rw₂ : Wbtw R x y z ∧ p -ᵥ y ≠ p -ᵥ x ∧ p -ᵥ y ≠ p -ᵥ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Tactic: rw [Sbtw, Sbtw, wbtw_const_vsub_iff, (vsub_right_injective p).ne_iff,
    (vsub_right_injective p).ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z p : 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
⊢ Sbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Sbtw R x y z
have rw₃ : Wbtw R x y z ∧ y ≠ x ∧ p -ᵥ y ≠ p -ᵥ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Tactic: rw [Sbtw, Sbtw, wbtw_const_vsub_iff, (vsub_right_injective p).ne_iff,
    (vsub_right_injective p).ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z p : 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
⊢ Sbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Sbtw R x y z
have rw₄ : Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Tactic: rw [Sbtw, Sbtw, wbtw_const_vsub_iff, (vsub_right_injective p).ne_iff,
    (vsub_right_injective p).ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z p : P
⊢ Sbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Sbtw R x y z
have rw : Wbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ∧ y -ᵥ p ≠ 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z p : P
rw : Wbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ∧ y -ᵥ p ≠ x -ᵥ p ∧ y -ᵥ p ≠ z -ᵥ p ↔ Sbtw R x y z
⊢ Sbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Sbtw R x y z
have 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
Tactic: rw [Sbtw, Sbtw, wbtw_vsub_const_iff, (vsub_left_injective p).ne_iff,
    (vsub_left_injective p).ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z p : 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
⊢ Sbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Sbtw R x y z
have rw₂ : Wbtw R x y z ∧ y -ᵥ p ≠ x -ᵥ p ∧ y -ᵥ p ≠ z -ᵥ p ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Tactic: rw [Sbtw, Sbtw, wbtw_vsub_const_iff, (vsub_left_injective p).ne_iff,
    (vsub_left_injective p).ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
x y z p : 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
⊢ Sbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Sbtw R x y z
have rw₃ : Wbtw R x y z ∧ y ≠ x ∧ y -ᵥ p ≠ z -ᵥ p ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Tactic: rw [Sbtw, Sbtw, wbtw_vsub_const_iff, (vsub_left_injective p).ne_iff,
    (vsub_left_injective p).ne_iff]