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 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂) (t.points i₃)
w : Fin (HAdd.hAdd (α := ℕ) 2 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ i : Fin (2 + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R (Set.range t.points))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i₂ i₃ r₁) :
            P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₂' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (t.points i₂) (singleton (α := P) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂ : P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
h₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₁) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hss : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₃) : SignType) (1 : SignType)
hs' :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (∑ i : Fin 3, w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hs : ∀ (i : Fin 3), 0 < w i
⊢ w i₁ < 1
have hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ {i₁, i₂, i₃}, w i) 1
Tactic: rw [hu] at hw
Cleared hypotheses: hw, hp, h₁', h₂', h₁s, h₂s, hss, hs', 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 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂) (t.points i₃)
w : Fin (HAdd.hAdd (α := ℕ) 2 1) → R
hw : w i₁ + (w i₂ + w i₃) = 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R (Set.range t.points))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i₂ i₃ r₁) :
            P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₂' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (t.points i₂) (singleton (α := P) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂ : P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
h₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₁) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hss : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₃) : SignType) (1 : SignType)
hs' :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (∑ i : Fin 3, w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hs : ∀ (i : Fin 3), 0 < w i
⊢ w i₁ < 1
have by_contra : ∀ (hle : ¬w i₁ < 1), False
Tactic: by_contra hle
-- 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 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂) (t.points i₃)
w : Fin (HAdd.hAdd (α := ℕ) 2 1) → R
hw : w i₁ + (w i₂ + w i₃) = 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R (Set.range t.points))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i₂ i₃ r₁) :
            P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₂' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (t.points i₂) (singleton (α := P) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂ : P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
h₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₁) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hss : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₃) : SignType) (1 : SignType)
hs' :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (∑ i : Fin 3, w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hs : ∀ (i : Fin 3), 0 < w i
hle : ¬w i₁ < 1
⊢ False
have hle₁ : 1 ≤ w i₁
Tactic: rw [not_lt] at hle
Cleared hypotheses: hle
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x y z : R
hxz_1 : x ≤ z
hxz : x = z
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z
have inl : ∀ (hxz : x ≤ x), Wbtw R x y x ↔ x ≤ y ∧ y ≤ x
Tactic: subst hxz
Cleared hypotheses: z, hxz_1, hxz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x y : R
hxz : x ≤ x
⊢ Wbtw R x y x ↔ x ≤ y ∧ y ≤ x
have inl : Wbtw R x y x ↔ x = y
Tactic: rw [← le_antisymm_iff, wbtw_self_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x y : R
hxz : x ≤ x
inl : Wbtw R x y x ↔ x = y
⊢ Wbtw R x y x ↔ x ≤ y ∧ y ≤ x
have inl₁ : y = x ↔ x = y
Tactic: rw [← le_antisymm_iff, wbtw_self_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x y : R
hxz : x ≤ x
inl : Wbtw R x y x ↔ x = y
inl₁ : y = x ↔ x = y
⊢ Wbtw R x y x ↔ x ≤ y ∧ y ≤ x
have inl₂ : x = y ↔ x = y
Tactic: rw [← le_antisymm_iff, wbtw_self_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x y z : R
hxz_1 : x ≤ z
hxz : x < z
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z
have hxz' : 0 < z - x
Tactic: have hxz' : 0 < z - x := sub_pos.mpr hxz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x y z : R
hxz_1 : x ≤ z
hxz : x < z
hxz' : 0 < z - x
r : R := (y - x) / (z - x)
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z
have hy : y = r * (z - x) + x
Tactic: have hy : y = r * (z - x) + x := by simp [r, hxz'.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x y z : R
hxz : x ≤ z
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z
have x₁ : x = z ∨ x < z
Tactic: cases hxz.eq_or_lt with
  | inl hxz =>
    subst hxz
    rw [← le_antisymm_iff, wbtw_self_iff, eq_comm]
  | inr hxz =>
    have hxz' : 0 < z - x := sub_pos.mpr hxz
    let r := (y - x) / (z - x)
    have hy : y = r * (z - x) + x := by simp [r, hxz'.ne']
    simp [hy, wbtw_mul_sub_add_iff, mul_nonneg_iff_of_pos_right hxz', ← le_sub_iff_add_le,
      mul_le_iff_le_one_left hxz', hxz.ne]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
⊢ Wbtw R x y z ↔
    x = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ici 1)) z
have refine_1 : ∀ (h : Wbtw R x y z),
  x = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ici 1)) z
Tactic: refine ⟨fun h => ?_, fun 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 : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
refine_1 :
  ∀ (h : Wbtw R x y z),
    x = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ici 1)) z
⊢ Wbtw R x y z ↔
    x = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ici 1)) z
have refine_2 : ∀
  (h :
    x = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ici 1)) z),
  Wbtw R x y z
Tactic: refine ⟨fun h => ?_, fun 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 : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
h : Wbtw R x y z
⊢ x = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ici 1)) z
have refine_1 : ∀ (r : R) (hr0 : 0 ≤ r) (hr1 : r ≤ 1),
  x = (lineMap x z : (a : R) → P) r ∨
    Membership.mem (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x ((lineMap x z : (a : R) → P) r)) : (a : R) → P) (Set.Ici 1)) z
Tactic: rcases h with ⟨r, ⟨hr0, hr1⟩, rfl⟩
Cleared hypotheses: y, 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 : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
⊢ x = (lineMap x z : (a : R) → P) r ∨
    Membership.mem (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x ((lineMap x z : (a : R) → P) r)) : (a : R) → P) (Set.Ici 1)) z
have refine_1 : ∀ (hr0' : 0 < r),
  x = (lineMap x z : (a : R) → P) r ∨
    Membership.mem (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x ((lineMap x z : (a : R) → P) r)) : (a : R) → P) (Set.Ici 1)) z
Tactic: rcases hr0.lt_or_eq with (hr0' | rfl)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
refine_1 :
  ∀ (hr0' : 0 < r),
    x = (lineMap x z : (a : R) → P) r ∨
      Membership.mem (γ := Set P)
        (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x ((lineMap x z : (a : R) → P) r)) : (a : R) → P) (Set.Ici 1)) z
⊢ x = (lineMap x z : (a : R) → P) r ∨
    Membership.mem (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x ((lineMap x z : (a : R) → P) r)) : (a : R) → P) (Set.Ici 1)) z
have refine_1₁ : ∀ (hr0 : LE.le.{u_1} (α := R) 0 0) (hr1 : LE.le.{u_1} (α := R) 0 1),
  x = (lineMap x z : (a : R) → P) 0 ∨
    Membership.mem (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x ((lineMap x z : (a : R) → P) 0)) : (a : R) → P) (Set.Ici 1)) z
Tactic: rcases hr0.lt_or_eq with (hr0' | rfl)
Cleared hypotheses: r, hr0, hr1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ x = (lineMap x z : (a : R) → P) r ∨
    ∃ (x_1 : R),
      Membership.mem (γ := Set R) (Set.Ici 1) x_1 ∧ (lineMap x ((lineMap x z : (a : R) → P) r) : (a : R) → P) x_1 = z
have refine_1 : (lineMap x ((lineMap x z : (a : R) → P) r) : (a : R) → P) r⁻¹ = z
Tactic: refine .inr ⟨r⁻¹, (one_le_inv₀ hr0').2 hr1, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ (lineMap x ((lineMap x z : (a : R) → P) r) : (a : R) → P) r⁻¹ = z
have refine_1 : (r⁻¹ * r) • (z -ᵥ x) +ᵥ x = z
Tactic: simp only [lineMap_apply, smul_smul, vadd_vsub]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ (r⁻¹ * r) • (z -ᵥ x) +ᵥ x = z
have refine_1 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (z -ᵥ x) +ᵥ x = z
Tactic: rw [inv_mul_cancel₀ hr0'.ne', one_smul, vsub_vadd]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
refine_1 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (z -ᵥ x) +ᵥ x = z
⊢ (r⁻¹ * r) • (z -ᵥ x) +ᵥ x = z
have refine_1₁ : (z -ᵥ x) +ᵥ x = z
Tactic: rw [inv_mul_cancel₀ hr0'.ne', one_smul, vsub_vadd]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
refine_1 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (z -ᵥ x) +ᵥ x = z
refine_1₁ : (z -ᵥ x) +ᵥ x = z
⊢ (r⁻¹ * r) • (z -ᵥ x) +ᵥ x = z
have refine_1₂ : z = z
Tactic: rw [inv_mul_cancel₀ hr0'.ne', one_smul, vsub_vadd]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
h : x = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ici 1)) z
⊢ Wbtw R x y z
have refine_2 : Wbtw R x x z
Tactic: rcases h with (rfl | ⟨r, ⟨hr, rfl⟩⟩)
Cleared hypotheses: y, 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 : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
h : x = y ∨ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ici 1)) z
refine_2 : Wbtw R x x z
⊢ Wbtw R x y z
have refine_2₁ : ∀ (r : R) (hr : Membership.mem (γ := Set R) (Set.Ici 1) r), Wbtw R x y ((lineMap x y : (a : R) → P) r)
Tactic: rcases h with (rfl | ⟨r, ⟨hr, rfl⟩⟩)
Cleared hypotheses: z, 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 : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
r : R
hr : Membership.mem (γ := Set R) (Set.Ici 1) r
⊢ Wbtw R x y ((lineMap x y : (a : R) → P) r)
have hr₁ : 1 ≤ r
Tactic: rw [Set.mem_Ici] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
⊢ Wbtw R x y ((lineMap x y : (a : R) → P) r)
have refine_2 : (lineMap x ((lineMap x y : (a : R) → P) r) : (a : R) → P) r⁻¹ = y
Tactic: refine ⟨r⁻¹, ⟨inv_nonneg.2 (zero_le_one.trans hr), inv_le_one_of_one_le₀ hr⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
⊢ (lineMap x ((lineMap x y : (a : R) → P) r) : (a : R) → P) r⁻¹ = y
have refine_2 : (r⁻¹ * r) • (y -ᵥ x) +ᵥ x = y
Tactic: simp only [lineMap_apply, smul_smul, vadd_vsub]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
⊢ (r⁻¹ * r) • (y -ᵥ x) +ᵥ x = y
have refine_2 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (y -ᵥ x) +ᵥ x = y
Tactic: rw [inv_mul_cancel₀ (one_pos.trans_le hr).ne', one_smul, vsub_vadd]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
refine_2 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (y -ᵥ x) +ᵥ x = y
⊢ (r⁻¹ * r) • (y -ᵥ x) +ᵥ x = y
have refine_2₁ : (y -ᵥ x) +ᵥ x = y
Tactic: rw [inv_mul_cancel₀ (one_pos.trans_le hr).ne', one_smul, vsub_vadd]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
refine_2 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (y -ᵥ x) +ᵥ x = y
refine_2₁ : (y -ᵥ x) +ᵥ x = y
⊢ (r⁻¹ * r) • (y -ᵥ x) +ᵥ x = y
have refine_2₂ : y = y
Tactic: rw [inv_mul_cancel₀ (one_pos.trans_le hr).ne', one_smul, vsub_vadd]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
h : Wbtw R x y z
hne : x ≠ y
⊢ Membership.mem (γ := AffineSubspace R P) (affineSpan R {x, y}) z
have rcases : ∀ (r : R) (h : Wbtw R x y ((lineMap x y : (a : R) → P) r)),
  Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R {x, y}) ((lineMap x y : (a : R) → P) r : P)
Tactic: rcases h.right_mem_image_Ici_of_left_ne hne with ⟨r, ⟨-, rfl⟩⟩
Cleared hypotheses: z, 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 : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
⊢ Sbtw R x y z ↔
    x ≠ y ∧ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) z
have refine_1 : ∀ (h : Sbtw R x y z),
  Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) z
Tactic: refine ⟨fun h => ⟨h.left_ne, ?_⟩, fun 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 : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
refine_1 :
  ∀ (h : Sbtw R x y z),
    Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) z
⊢ Sbtw R x y z ↔
    x ≠ y ∧ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) z
have refine_2 : ∀
  (h :
    x ≠ y ∧ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) z),
  Sbtw R x y z
Tactic: refine ⟨fun h => ⟨h.left_ne, ?_⟩, fun 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 : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y z : P
h : Sbtw R x y z
⊢ Membership.mem (γ := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) z
have refine_1 : ∀ (r : R) (hr : Membership.mem (γ := Set R) (Set.Ici 1) r) (h : Sbtw R x y ((lineMap x y : (a : R) → P) r)),
  Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) ((lineMap x y : (a : R) → P) r : P)
Tactic: obtain ⟨r, ⟨hr, rfl⟩⟩ := h.wbtw.right_mem_image_Ici_of_left_ne h.left_ne
Cleared hypotheses: z, 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 : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
r : R
hr : Membership.mem (γ := Set R) (Set.Ici 1) r
h : Sbtw R x y ((lineMap x y : (a : R) → P) r)
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) ((lineMap x y : (a : R) → P) r : P)
have hr₁ : 1 ≤ r
Tactic: rw [Set.mem_Ici] at hr
Cleared hypotheses: hr, 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 : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
h : Sbtw R x y ((lineMap x y : (a : R) → P) r)
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) ((lineMap x y : (a : R) → P) r : P)
have refine_1 : ∀ (hrlt : 1 < r),
  Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
    (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioi 1)) ((lineMap x y : (a : R) → P) r : P)
Tactic: rcases hr.lt_or_eq with (hrlt | rfl)