awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p = p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
have h₁ : p₂ = p₃
Tactic: rw [vsub_left_cancel_iff] at h
Cleared hypotheses: h, hp₂p₁, hp₂p₃
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p ∈ openSegment ℝ (p₁ -ᵥ p) (p₃ -ᵥ p)
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
have h₁ : ∃ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) x ∧ (1 - x) • (p₁ -ᵥ p) + x • (p₃ -ᵥ p) = p₂ -ᵥ p
Tactic: rw [openSegment_eq_image, Set.mem_image] at h
Cleared hypotheses: h, hp₂p₁, hp₂p₃
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : ∃ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) x ∧ (1 - x) • (p₁ -ᵥ p) + x • (p₃ -ᵥ p) = p₂ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
have inr : ∀ (r : ℝ) (hr : (1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p) = p₂ -ᵥ p) (hr0 : 0 < r) (hr1 : r < 1),
  dist p₂ p < max (dist p₁ p) (dist p₃ p)
Tactic: rcases h with ⟨r, ⟨hr0, hr1⟩, hr⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
r : ℝ
hr : (1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p) = p₂ -ᵥ p
hr0 : 0 < r
hr1 : r < 1
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
have inr : ‖(1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p)‖ < max ‖p₁ -ᵥ p‖ ‖p₃ -ᵥ p‖
Tactic: simp_rw [@dist_eq_norm_vsub V, ← hr]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
have pos : ∀ (hp₁ : p₂ = p₁), dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
Tactic: by_cases hp₁ : p₂ = p₁
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
pos : ∀ (hp₁ : p₂ = p₁), dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
have neg : ∀ (hp₁ : ¬p₂ = p₁), dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
Tactic: by_cases hp₁ : p₂ = p₁
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₁ : ¬p₂ = p₁
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
have pos : ∀ (hp₃ : p₂ = p₃), dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
Tactic: by_cases hp₃ : p₂ = p₃
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₁ : ¬p₂ = p₁
pos : ∀ (hp₃ : p₂ = p₃), dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
have neg : ∀ (hp₃ : ¬p₂ = p₃), dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
Tactic: by_cases hp₃ : p₂ = p₃
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₁ : ¬p₂ = p₁
hp₃ : ¬p₂ = p₃
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
have hs : Sbtw ℝ p₁ p₂ p₃
Tactic: have hs : Sbtw ℝ p₁ p₂ p₃ := ⟨h, hp₁, hp₃⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
⊢ Wbtw ℝ p₁ p₂ p₃
have inl : ∀ (hw : Wbtw ℝ p₁ p₂ p₃), Wbtw ℝ p₁ p₂ p₃
Tactic: rcases h.wbtw_or_wbtw_or_wbtw with (hw | hw | hw)
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
inl : ∀ (hw : Wbtw ℝ p₁ p₂ p₃), Wbtw ℝ p₁ p₂ p₃
⊢ Wbtw ℝ p₁ p₂ p₃
have inr : ∀ (hw : Wbtw ℝ p₂ p₃ p₁), Wbtw ℝ p₁ p₂ p₃
Tactic: rcases h.wbtw_or_wbtw_or_wbtw with (hw | hw | hw)
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
inl : ∀ (hw : Wbtw ℝ p₁ p₂ p₃), Wbtw ℝ p₁ p₂ p₃
inr : ∀ (hw : Wbtw ℝ p₂ p₃ p₁), Wbtw ℝ p₁ p₂ p₃
⊢ Wbtw ℝ p₁ p₂ p₃
have inr₁ : ∀ (hw : Wbtw ℝ p₃ p₁ p₂), Wbtw ℝ p₁ p₂ p₃
Tactic: rcases h.wbtw_or_wbtw_or_wbtw with (hw | hw | hw)
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
⊢ Wbtw ℝ p₁ p₂ p₃
have pos : ∀ (hp₃p₂ : p₃ = p₂), Wbtw ℝ p₁ p₂ p₃
Tactic: by_cases hp₃p₂ : p₃ = p₂
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
pos : ∀ (hp₃p₂ : p₃ = p₂), Wbtw ℝ p₁ p₂ p₃
⊢ Wbtw ℝ p₁ p₂ p₃
have neg : ∀ (hp₃p₂ : ¬p₃ = p₂), Wbtw ℝ p₁ p₂ p₃
Tactic: by_cases hp₃p₂ : p₃ = p₂
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : ¬p₃ = p₂
⊢ Wbtw ℝ p₁ p₂ p₃
have hs : Sbtw ℝ p₂ p₃ p₁
Tactic: have hs : Sbtw ℝ p₂ p₃ p₁ := ⟨hw, hp₃p₂, hp₁p₃.symm⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : ¬p₃ = p₂
hs : Sbtw ℝ p₂ p₃ p₁
⊢ Wbtw ℝ p₁ p₂ p₃
have hs' : dist p₃ p < max (dist p₂ p) (dist p₁ p)
Tactic: have hs' := hs.dist_lt_max_dist p
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : ¬p₃ = p₂
hs : Sbtw ℝ p₂ p₃ p₁
hs' : dist p₃ p < max (dist p₂ p) (dist p₁ p)
⊢ Wbtw ℝ p₁ p₂ p₃
have hs'₁ : r < dist p₂ p
Tactic: rw [hp₁, hp₃, lt_max_iff, lt_self_iff_false, or_false] at hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
⊢ Wbtw ℝ p₁ p₂ p₃
have pos : ∀ (hp₁p₂ : p₁ = p₂), Wbtw ℝ p₁ p₂ p₃
Tactic: by_cases hp₁p₂ : p₁ = p₂
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
pos : ∀ (hp₁p₂ : p₁ = p₂), Wbtw ℝ p₁ p₂ p₃
⊢ Wbtw ℝ p₁ p₂ p₃
have neg : ∀ (hp₁p₂ : ¬p₁ = p₂), Wbtw ℝ p₁ p₂ p₃
Tactic: by_cases hp₁p₂ : p₁ = p₂
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : ¬p₁ = p₂
⊢ Wbtw ℝ p₁ p₂ p₃
have hs : Sbtw ℝ p₃ p₁ p₂
Tactic: have hs : Sbtw ℝ p₃ p₁ p₂ := ⟨hw, hp₁p₃, hp₁p₂⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : ¬p₁ = p₂
hs : Sbtw ℝ p₃ p₁ p₂
⊢ Wbtw ℝ p₁ p₂ p₃
have hs' : dist p₁ p < max (dist p₃ p) (dist p₂ p)
Tactic: have hs' := hs.dist_lt_max_dist p
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ (P := P) {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : ¬p₁ = p₂
hs : Sbtw ℝ p₃ p₁ p₂
hs' : dist p₁ p < max (dist p₃ p) (dist p₂ p)
⊢ Wbtw ℝ p₁ p₂ p₃
have hs'₁ : r < dist p₂ p
Tactic: rw [hp₁, hp₃, lt_max_iff, lt_self_iff_false, false_or] at hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
a b c : P
⊢ dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c
have this : dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔ b -ᵥ a ∈ [a -ᵥ a -[ℝ] c -ᵥ a]
Tactic: have :
      dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔
        b -ᵥ a ∈ segment ℝ (a -ᵥ a) (c -ᵥ a) := by
    simp only [mem_segment_iff_sameRay, sameRay_iff_norm_add, dist_eq_norm', sub_add_sub_cancel',
      eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
a b c : P
this : dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔ b -ᵥ a ∈ [a -ᵥ a -[ℝ] c -ᵥ a]
⊢ dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c
have this₁ : dist a b + dist b c = dist a c ↔ Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ a) '' affineSegment ℝ a c) (b -ᵥ a)
Tactic: simp_rw [dist_vsub_cancel_right, ← affineSegment_eq_segment, ← affineSegment_vsub_const_image]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
a b c : P
this :
  dist a b + dist b c = dist a c ↔ Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ a) '' affineSegment ℝ a c) (b -ᵥ a)
⊢ dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c
have rwa : ∀ (this : dist a b + dist b c = dist a c ↔ b ∈ affineSegment ℝ a c), dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c
Tactic: rwa [(vsub_left_injective _).mem_set_image] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
a b c : P
⊢ dist a c < dist a b + dist b c ↔ ¬Wbtw ℝ a b c
have rw : dist a c ≠ dist a b + dist b c ↔ ¬Wbtw ℝ a b c
Tactic: rw [← ne_iff_lt_iff_le.mpr (dist_triangle _ _ _), not_iff_not, eq_comm, dist_add_dist_eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
a b c : P
rw : dist a c ≠ dist a b + dist b c ↔ ¬Wbtw ℝ a b c
⊢ dist a c < dist a b + dist b c ↔ ¬Wbtw ℝ a b c
have rw₁ : dist a c = dist a b + dist b c ↔ Wbtw ℝ a b c
Tactic: rw [← ne_iff_lt_iff_le.mpr (dist_triangle _ _ _), not_iff_not, eq_comm, dist_add_dist_eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
a b c : P
rw : dist a c ≠ dist a b + dist b c ↔ ¬Wbtw ℝ a b c
rw₁ : dist a c = dist a b + dist b c ↔ Wbtw ℝ a b c
⊢ dist a c < dist a b + dist b c ↔ ¬Wbtw ℝ a b c
have rw₂ : dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c
Tactic: rw [← ne_iff_lt_iff_le.mpr (dist_triangle _ _ _), not_iff_not, eq_comm, dist_add_dist_eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
a b c : P
rw : dist a c ≠ dist a b + dist b c ↔ ¬Wbtw ℝ a b c
rw₁ : dist a c = dist a b + dist b c ↔ Wbtw ℝ a b c
rw₂ : dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c
⊢ dist a c < dist a b + dist b c ↔ ¬Wbtw ℝ a b c
have rw₃ : Wbtw ℝ a b c ↔ Wbtw ℝ a b c
Tactic: rw [← ne_iff_lt_iff_le.mpr (dist_triangle _ _ _), not_iff_not, eq_comm, dist_add_dist_eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
⊢ y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
have rw : Wbtw ℝ 0 (y -ᵥ x) (z -ᵥ x)
Tactic: rw [mem_segment_iff_wbtw, ← dist_add_dist_eq_iff, dist_zero, dist_vsub_cancel_right,
      ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy, hyz, ← add_mul, add_sub_cancel,
      one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
rw : Wbtw ℝ 0 (y -ᵥ x) (z -ᵥ x)
⊢ y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
have rw₁ : dist 0 (y -ᵥ x) + dist (y -ᵥ x) (z -ᵥ x) = dist 0 (z -ᵥ x)
Tactic: rw [mem_segment_iff_wbtw, ← dist_add_dist_eq_iff, dist_zero, dist_vsub_cancel_right,
      ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy, hyz, ← add_mul, add_sub_cancel,
      one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
rw : Wbtw ℝ 0 (y -ᵥ x) (z -ᵥ x)
rw₁ : dist 0 (y -ᵥ x) + dist (y -ᵥ x) (z -ᵥ x) = dist 0 (z -ᵥ x)
⊢ y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
have rw₂ : ‖y -ᵥ x‖ + dist (y -ᵥ x) (z -ᵥ x) = ‖z -ᵥ x‖
Tactic: rw [mem_segment_iff_wbtw, ← dist_add_dist_eq_iff, dist_zero, dist_vsub_cancel_right,
      ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy, hyz, ← add_mul, add_sub_cancel,
      one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
rw : Wbtw ℝ 0 (y -ᵥ x) (z -ᵥ x)
rw₁ : dist 0 (y -ᵥ x) + dist (y -ᵥ x) (z -ᵥ x) = dist 0 (z -ᵥ x)
rw₂ : ‖y -ᵥ x‖ + dist (y -ᵥ x) (z -ᵥ x) = ‖z -ᵥ x‖
⊢ y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
have rw₃ : ‖y -ᵥ x‖ + dist y z = ‖z -ᵥ x‖
Tactic: rw [mem_segment_iff_wbtw, ← dist_add_dist_eq_iff, dist_zero, dist_vsub_cancel_right,
      ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy, hyz, ← add_mul, add_sub_cancel,
      one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
rw : Wbtw ℝ 0 (y -ᵥ x) (z -ᵥ x)
rw₁ : dist 0 (y -ᵥ x) + dist (y -ᵥ x) (z -ᵥ x) = dist 0 (z -ᵥ x)
rw₂ : ‖y -ᵥ x‖ + dist (y -ᵥ x) (z -ᵥ x) = ‖z -ᵥ x‖
rw₃ : ‖y -ᵥ x‖ + dist y z = ‖z -ᵥ x‖
⊢ y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
have rw₄ : dist x y + dist y z = ‖z -ᵥ x‖
Tactic: rw [mem_segment_iff_wbtw, ← dist_add_dist_eq_iff, dist_zero, dist_vsub_cancel_right,
      ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy, hyz, ← add_mul, add_sub_cancel,
      one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
rw : Wbtw ℝ 0 (y -ᵥ x) (z -ᵥ x)
rw₁ : dist 0 (y -ᵥ x) + dist (y -ᵥ x) (z -ᵥ x) = dist 0 (z -ᵥ x)
rw₂ : ‖y -ᵥ x‖ + dist (y -ᵥ x) (z -ᵥ x) = ‖z -ᵥ x‖
rw₃ : ‖y -ᵥ x‖ + dist y z = ‖z -ᵥ x‖
rw₄ : dist x y + dist y z = ‖z -ᵥ x‖
⊢ y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
have rw₅ : dist x y + dist y z = dist x z
Tactic: rw [mem_segment_iff_wbtw, ← dist_add_dist_eq_iff, dist_zero, dist_vsub_cancel_right,
      ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy, hyz, ← add_mul, add_sub_cancel,
      one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
rw : Wbtw ℝ 0 (y -ᵥ x) (z -ᵥ x)
rw₁ : dist 0 (y -ᵥ x) + dist (y -ᵥ x) (z -ᵥ x) = dist 0 (z -ᵥ x)
rw₂ : ‖y -ᵥ x‖ + dist (y -ᵥ x) (z -ᵥ x) = ‖z -ᵥ x‖
rw₃ : ‖y -ᵥ x‖ + dist y z = ‖z -ᵥ x‖
rw₄ : dist x y + dist y z = ‖z -ᵥ x‖
rw₅ : dist x y + dist y z = dist x z
⊢ y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
have rw₆ : r * dist x z + dist y z = dist x z
Tactic: rw [mem_segment_iff_wbtw, ← dist_add_dist_eq_iff, dist_zero, dist_vsub_cancel_right,
      ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy, hyz, ← add_mul, add_sub_cancel,
      one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
rw : Wbtw ℝ 0 (y -ᵥ x) (z -ᵥ x)
rw₁ : dist 0 (y -ᵥ x) + dist (y -ᵥ x) (z -ᵥ x) = dist 0 (z -ᵥ x)
rw₂ : ‖y -ᵥ x‖ + dist (y -ᵥ x) (z -ᵥ x) = ‖z -ᵥ x‖
rw₃ : ‖y -ᵥ x‖ + dist y z = ‖z -ᵥ x‖
rw₄ : dist x y + dist y z = ‖z -ᵥ x‖
rw₅ : dist x y + dist y z = dist x z
rw₆ : r * dist x z + dist y z = dist x z
⊢ y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
have rw₇ : r * dist x z + (1 - r) * dist x z = dist x z
Tactic: rw [mem_segment_iff_wbtw, ← dist_add_dist_eq_iff, dist_zero, dist_vsub_cancel_right,
      ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy, hyz, ← add_mul, add_sub_cancel,
      one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
rw : Wbtw ℝ 0 (y -ᵥ x) (z -ᵥ x)
rw₁ : dist 0 (y -ᵥ x) + dist (y -ᵥ x) (z -ᵥ x) = dist 0 (z -ᵥ x)
rw₂ : ‖y -ᵥ x‖ + dist (y -ᵥ x) (z -ᵥ x) = ‖z -ᵥ x‖
rw₃ : ‖y -ᵥ x‖ + dist y z = ‖z -ᵥ x‖
rw₄ : dist x y + dist y z = ‖z -ᵥ x‖
rw₅ : dist x y + dist y z = dist x z
rw₆ : r * dist x z + dist y z = dist x z
rw₇ : r * dist x z + (1 - r) * dist x z = dist x z
⊢ y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
have rw₈ : (r + (1 - r)) * dist x z = dist x z
Tactic: rw [mem_segment_iff_wbtw, ← dist_add_dist_eq_iff, dist_zero, dist_vsub_cancel_right,
      ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy, hyz, ← add_mul, add_sub_cancel,
      one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
rw : Wbtw ℝ 0 (y -ᵥ x) (z -ᵥ x)
rw₁ : dist 0 (y -ᵥ x) + dist (y -ᵥ x) (z -ᵥ x) = dist 0 (z -ᵥ x)
rw₂ : ‖y -ᵥ x‖ + dist (y -ᵥ x) (z -ᵥ x) = ‖z -ᵥ x‖
rw₃ : ‖y -ᵥ x‖ + dist y z = ‖z -ᵥ x‖
rw₄ : dist x y + dist y z = ‖z -ᵥ x‖
rw₅ : dist x y + dist y z = dist x z
rw₆ : r * dist x z + dist y z = dist x z
rw₇ : r * dist x z + (1 - r) * dist x z = dist x z
rw₈ : (r + (1 - r)) * dist x z = dist x z
⊢ y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
have rw₉ : 1 * dist x z = dist x z
Tactic: rw [mem_segment_iff_wbtw, ← dist_add_dist_eq_iff, dist_zero, dist_vsub_cancel_right,
      ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy, hyz, ← add_mul, add_sub_cancel,
      one_mul]