awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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
⊢ x = (lineMap x z : (a : R) → P) ty
have hx₁ : 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
Cleared hypotheses: hx
-- 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
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
⊢ x = (lineMap x z : (a : R) → P) ty
have mp : ∀ (h : tx - tx * ty + ty = 0), x = (lineMap x z : (a : R) → P) ty
Tactic: rcases hx with (h | h)
Cleared hypotheses: hx
-- 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
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
⊢ x = (lineMap x z : (a : R) → P) ty
have mp₁ : ∀ (h : z -ᵥ x = 0), x = (lineMap x z : (a : R) → P) ty
Tactic: rcases hx with (h | h)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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
⊢ x = (lineMap x z : (a : R) → P) ty
have h₁ : tx * 1 - tx * ty + ty = 0
Tactic: nth_rw 1 [← mul_one tx] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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
⊢ x = (lineMap x z : (a : R) → P) ty
have h₁ : -(tx * (1 - ty)) = ty
Tactic: rw [← mul_sub, add_eq_zero_iff_neg_eq] at h
Cleared hypotheses: h
-- 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
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
have refine : ty ≤ 0
Tactic: refine le_antisymm ?_ hty.1
-- 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
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
have rw : 0 ≤ tx * (1 - ty)
Tactic: rw [← h, Left.neg_nonpos_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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
⊢ x = (lineMap x z : (a : R) → P) ty
have h' : 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)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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
⊢ x = (lineMap x z : (a : R) → P) ty
have h₁ : z = x
Tactic: rw [vsub_eq_zero_iff_eq] at h
Cleared hypotheses: h
-- 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
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
⊢ x = (lineMap x z : (a : R) → P) ty
have mp : x = (lineMap x x : (a : R) → P) ty
Tactic: rw [h, lineMap_same_apply]
-- 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
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
⊢ x = (lineMap x z : (a : R) → P) ty
have mp₁ : x = x
Tactic: rw [h, lineMap_same_apply]
-- 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
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
⊢ Wbtw R x y z ∧ Wbtw R x z y ↔ y = z
have rw : Wbtw R z y x ∧ Wbtw R y z x ↔ z = y
Tactic: rw [wbtw_comm, wbtw_comm (z := y), eq_comm]
-- 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
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
y z x : P
⊢ Wbtw R x y z ∧ Wbtw R z x y ↔ x = y
have rw : Wbtw R z y x ∧ Wbtw R z x y ↔ x = y
Tactic: rw [wbtw_comm, wbtw_swap_right_iff, eq_comm]
-- 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
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
⊢ Wbtw R x y z ∧ Wbtw R z x y ↔ x = y
have rw₁ : y = x ↔ x = y
Tactic: rw [wbtw_comm, wbtw_swap_right_iff, eq_comm]
-- 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
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
⊢ Wbtw R x y z ∧ Wbtw R z x y ↔ x = y
have rw₂ : x = y ↔ x = y
Tactic: rw [wbtw_comm, wbtw_swap_right_iff, eq_comm]
-- 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
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
h : Wbtw R x y z
⊢ Wbtw R y x z ↔ x = y
have rw : Wbtw R y x z ↔ Wbtw R x y z ∧ Wbtw R y x z
Tactic: rw [← wbtw_swap_left_iff R z, and_iff_right h]
-- 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
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
⊢ Wbtw R y x z ↔ x = y
have rw₁ : Wbtw R y x z ↔ Wbtw R y x z
Tactic: rw [← wbtw_swap_left_iff R z, and_iff_right h]
-- 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
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
h : Wbtw R x y z
⊢ Wbtw R x z y ↔ y = z
have rw : Wbtw R x z y ↔ Wbtw R x y z ∧ Wbtw R x z y
Tactic: rw [← wbtw_swap_right_iff R x, and_iff_right h]
-- 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
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
⊢ Wbtw R x z y ↔ y = z
have rw₁ : Wbtw R x z y ↔ Wbtw R x z y
Tactic: rw [← wbtw_swap_right_iff R x, and_iff_right h]
-- 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
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y z : P
h : Wbtw R x y z
⊢ Wbtw R z x y ↔ x = y
have rw : Wbtw R z x y ↔ Wbtw R x y z ∧ Wbtw R z x y
Tactic: rw [← wbtw_rotate_iff R x, and_iff_right h]
-- 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
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
⊢ Wbtw R z x y ↔ x = y
have rw₂ : Wbtw R z x y ↔ Wbtw R z x y
Tactic: rw [← wbtw_rotate_iff R x, and_iff_right h]
-- 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
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y : P
r : R
⊢ Wbtw R x ((lineMap x y : (a : R) → P) r) y ↔ x = y ∨ Membership.mem (γ := Set R) (Set.Icc 0 1) r
have 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
Tactic: by_cases hxy : x = y
-- 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
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
⊢ Wbtw R x ((lineMap x y : (a : R) → P) r) y ↔ x = y ∨ Membership.mem (γ := Set R) (Set.Icc 0 1) r
have 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
Tactic: by_cases hxy : x = y
-- 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
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y : P
r : R
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
have pos : Wbtw R y y y ↔ y = y ∨ Membership.mem (γ := Set R) (Set.Icc 0 1) r
Tactic: rw [hxy, lineMap_same_apply]
-- 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
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y : P
r : R
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
have neg : Wbtw R x ((lineMap x y : (a : R) → P) r) 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]
-- 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
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
⊢ Wbtw R x ((lineMap x y : (a : R) → P) r) y ↔ x = y ∨ Membership.mem (γ := Set R) (Set.Icc 0 1) r
have 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
Tactic: rw [or_iff_right hxy, Wbtw, affineSegment, (lineMap_injective R hxy).mem_set_image]
-- 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
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
⊢ Wbtw R x ((lineMap x y : (a : R) → P) r) y ↔ x = y ∨ Membership.mem (γ := Set R) (Set.Icc 0 1) r
have 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
Tactic: rw [or_iff_right hxy, Wbtw, affineSegment, (lineMap_injective R hxy).mem_set_image]
-- 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
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
⊢ Wbtw R x ((lineMap x y : (a : R) → P) r) y ↔ x = y ∨ Membership.mem (γ := Set R) (Set.Icc 0 1) r
have neg₃ : Membership.mem (γ := Set R) (Set.Icc 0 1) r ↔ Membership.mem (γ := Set R) (Set.Icc 0 1) r
Tactic: rw [or_iff_right hxy, Wbtw, affineSegment, (lineMap_injective R hxy).mem_set_image]
-- 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
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y : P
r : R
⊢ Sbtw R x ((lineMap x y : (a : R) → P) r) y ↔ x ≠ y ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
have rw : x ≠ y →
  (Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioo 0 1)) ((lineMap x y : (a : R) → P) r : P) ↔
    Membership.mem (γ := Set R) (Set.Ioo 0 1) r)
Tactic: rw [sbtw_iff_mem_image_Ioo_and_ne, and_comm, and_congr_right]
-- 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
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y : P
r : R
hxy : x ≠ y
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioo 0 1)) ((lineMap x y : (a : R) → P) r : P) ↔
    Membership.mem (γ := Set R) (Set.Ioo 0 1) r
have rw : Membership.mem (γ := Set R) (Set.Ioo 0 1) r ↔ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
Tactic: rw [(lineMap_injective R hxy).mem_set_image]
-- 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
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x y z : P
h₁ : Wbtw R w y z
h₂ : Sbtw R w x y
⊢ Sbtw R w x z
have refine : x ≠ z
Tactic: refine ⟨h₁.trans_left h₂.wbtw, h₂.ne_left, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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
w x y z : P
h₁ : Wbtw R w x z
h₂ : Sbtw R x y z
⊢ Sbtw R w y z
have h₃ : Wbtw R z x w
Tactic: rw [wbtw_comm] at *
Cleared hypotheses: h₁, h₂
-- 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
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x y z : P
h₁ : Wbtw R z x w
h₂ : Sbtw R x y z
⊢ Sbtw R w y z
have rw : ∀ (h₂ : Sbtw R z y x), Sbtw R z y w
Tactic: rw [sbtw_comm] at *
Cleared hypotheses: h₂
-- 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
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
h :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (α := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₁ : P)
        (singleton (α := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₂ : P))))
    ((Finset.affineCombination R s p : (a : ι → R) → P) w : P)
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
⊢ Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₁ : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w₂ : P)
have rw : ∀ (h : ∃ (r : R), ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i) {i : ι} (his : i ∈ s) (hs : Sbtw R (w₁ i) (w i) (w₂ i)),
  Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₁ : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w₂ : P)
Tactic: rw [affineCombination_mem_affineSpan_pair ha hw hw₁ hw₂] at h
Cleared hypotheses: h, i, his, hs
-- 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
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
h : ∃ (r : R), ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
⊢ Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₁ : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w₂ : P)
have rcases : ∀ (r : R) (hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i),
  Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₁ : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w₂ : P)
Tactic: rcases h with ⟨r, hr⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
r : R
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₁ : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w₂ : P)
have hs₁ : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
Tactic: rw [hr i his, sbtw_mul_sub_add_iff] at hs
Cleared hypotheses: hs, hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
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
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₁ : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w₂ : P)
have hr₁ : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
Tactic: change ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i at hr
Cleared hypotheses: hr