awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₉ : 1 * dist x z = dist x z
⊢ y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
have rw₁₀ : 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 (hypothesis)
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 = (AffineMap.lineMap x z : (a : ℝ) → PE) r
have this : y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
Tactic: have : y -ᵥ x ∈ [(0 : E) -[ℝ] z -ᵥ x] := by
    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
this : y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
⊢ y = (AffineMap.lineMap x z : (a : ℝ) → PE) r
have inl : ∀ (hxy : dist x y = r * dist x x) (hyz : dist y x = (1 - r) * dist x x) (this : y -ᵥ x ∈ [0 -[ℝ] x -ᵥ x]),
  y = (AffineMap.lineMap x x : (a : ℝ) → PE) r
Tactic: obtain rfl | hne := eq_or_ne x z
Cleared hypotheses: z, hxy, hyz, this
-- 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
this : y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
inl :
  ∀ (hxy : dist x y = r * dist x x) (hyz : dist y x = (1 - r) * dist x x) (this : y -ᵥ x ∈ [0 -[ℝ] x -ᵥ x]),
    y = (AffineMap.lineMap x x : (a : ℝ) → PE) r
⊢ y = (AffineMap.lineMap x z : (a : ℝ) → PE) r
have inr : ∀ (hne : x ≠ z), y = (AffineMap.lineMap x z : (a : ℝ) → PE) r
Tactic: obtain rfl | hne := eq_or_ne x z
-- 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 : PE
hxy : dist x y = r * dist x x
hyz : dist y x = (1 - r) * dist x x
this : y -ᵥ x ∈ [0 -[ℝ] x -ᵥ x]
⊢ y = (AffineMap.lineMap x x : (a : ℝ) → PE) r
have inl : ∀ (hxy : dist y y = r * dist y y) (hyz : dist y y = (1 - r) * dist y y) (this : y -ᵥ y ∈ [0 -[ℝ] y -ᵥ y]),
  y = (AffineMap.lineMap y y : (a : ℝ) → PE) r
Tactic: obtain rfl : y = x := by simpa
Cleared hypotheses: x, hxy, hyz, this
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (hypothesis)
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
this : y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
hne : x ≠ z
⊢ y = (AffineMap.lineMap x z : (a : ℝ) → PE) r
have hne₁ : dist x z ≠ 0
Tactic: rw [← dist_ne_zero] at hne
Cleared hypotheses: hne
-- 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
this : y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
hne : dist x z ≠ 0
⊢ y = (AffineMap.lineMap x z : (a : ℝ) → PE) r
have inr : ∀ (a b : ℝ),
  0 ≤ a →
    ∀ (hb : 0 ≤ b),
      a + b = 1 → ∀ (H : HSMul.hSMul (β := E) a 0 + b • (z -ᵥ x) = y -ᵥ x), y = (AffineMap.lineMap x z : (a : ℝ) → PE) r
Tactic: obtain ⟨a, b, _, hb, _, H⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (hypothesis)
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
hne : dist x z ≠ 0
a b : ℝ
left : 0 ≤ a
hb : 0 ≤ b
left_1 : a + b = 1
H : HSMul.hSMul (β := E) a 0 + b • (z -ᵥ x) = y -ᵥ x
⊢ y = (AffineMap.lineMap x z : (a : ℝ) → PE) r
have H₁ : b • (z -ᵥ x) = y -ᵥ x
Tactic: rw [smul_zero, zero_add] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (hypothesis)
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
hne : dist x z ≠ 0
a b : ℝ
left : 0 ≤ a
hb : 0 ≤ b
left_1 : a + b = 1
H : b • (z -ᵥ x) = y -ᵥ x
⊢ y = (AffineMap.lineMap x z : (a : ℝ) → PE) r
have H' : ‖b • (z -ᵥ x)‖ = ‖y -ᵥ x‖
Tactic: have H' := congr_arg norm H
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (hypothesis)
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
hne : dist x z ≠ 0
a b : ℝ
left : 0 ≤ a
hb : 0 ≤ b
left_1 : a + b = 1
H : b • (z -ᵥ x) = y -ᵥ x
H' : ‖b • (z -ᵥ x)‖ = ‖y -ᵥ x‖
⊢ y = (AffineMap.lineMap x z : (a : ℝ) → PE) r
have H'₁ : b = r
Tactic: rw [norm_smul, Real.norm_of_nonneg hb, ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy,
      mul_left_inj' hne] at H'
Cleared hypotheses: H'
-- 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
hne : dist x z ≠ 0
a b : ℝ
left : 0 ≤ a
hb : 0 ≤ b
left_1 : a + b = 1
H : b • (z -ᵥ x) = y -ᵥ x
H' : b = r
⊢ y = (AffineMap.lineMap x z : (a : ℝ) → PE) r
have inr : y = r • (z -ᵥ x) +ᵥ x
Tactic: rw [AffineMap.lineMap_apply, ← H', H, vsub_vadd]
-- 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
hne : dist x z ≠ 0
a b : ℝ
left : 0 ≤ a
hb : 0 ≤ b
left_1 : a + b = 1
H : b • (z -ᵥ x) = y -ᵥ x
H' : b = r
inr : y = r • (z -ᵥ x) +ᵥ x
⊢ y = (AffineMap.lineMap x z : (a : ℝ) → PE) r
have inr₁ : y = b • (z -ᵥ x) +ᵥ x
Tactic: rw [AffineMap.lineMap_apply, ← H', H, vsub_vadd]
-- 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
hne : dist x z ≠ 0
a b : ℝ
left : 0 ≤ a
hb : 0 ≤ b
left_1 : a + b = 1
H : b • (z -ᵥ x) = y -ᵥ x
H' : b = r
inr : y = r • (z -ᵥ x) +ᵥ x
inr₁ : y = b • (z -ᵥ x) +ᵥ x
⊢ y = (AffineMap.lineMap x z : (a : ℝ) → PE) r
have inr₂ : y = (y -ᵥ x) +ᵥ x
Tactic: rw [AffineMap.lineMap_apply, ← H', H, vsub_vadd]
-- 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
hne : dist x z ≠ 0
a b : ℝ
left : 0 ≤ a
hb : 0 ≤ b
left_1 : a + b = 1
H : b • (z -ᵥ x) = y -ᵥ x
H' : b = r
inr : y = r • (z -ᵥ x) +ᵥ x
inr₁ : y = b • (z -ᵥ x) +ᵥ x
inr₂ : y = (y -ᵥ x) +ᵥ x
⊢ y = (AffineMap.lineMap x z : (a : ℝ) → PE) r
have inr₃ : y = y
Tactic: rw [AffineMap.lineMap_apply, ← H', H, vsub_vadd]
-- 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
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
⊢ y = midpoint ℝ x z
have hxy : dist x y = @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * dist x z
Tactic: apply eq_lineMap_of_dist_eq_mul_of_dist_eq_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
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
hxy : dist x y = @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * dist x z
⊢ y = midpoint ℝ x z
have hyz : dist y z = HSub.hSub (α := ℝ) 1 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) * dist x z
Tactic: apply eq_lineMap_of_dist_eq_mul_of_dist_eq_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
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
⊢ dist x y = @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * dist x z
have hxy : dist x y = 2⁻¹ * dist x z
Tactic: rwa [invOf_eq_inv, ← div_eq_inv_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
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
⊢ dist y z = HSub.hSub (α := ℝ) 1 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) * dist x z
have hyz : dist y z = HSub.hSub (α := ℝ) 1 2⁻¹ * dist x z
Tactic: rwa [invOf_eq_inv, ← one_div, sub_half, one_div, ← div_eq_inv_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
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
hyz : dist y z = HSub.hSub (α := ℝ) 1 2⁻¹ * dist x z
⊢ dist y z = HSub.hSub (α := ℝ) 1 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) * dist x z
have hyz₁ : dist y z = (1 - 1 / 2) * dist x z
Tactic: rwa [invOf_eq_inv, ← one_div, sub_half, one_div, ← div_eq_inv_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
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
hyz : dist y z = HSub.hSub (α := ℝ) 1 2⁻¹ * dist x z
hyz₁ : dist y z = (1 - 1 / 2) * dist x z
⊢ dist y z = HSub.hSub (α := ℝ) 1 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) * dist x z
have hyz₂ : dist y z = 1 / 2 * dist x z
Tactic: rwa [invOf_eq_inv, ← one_div, sub_half, one_div, ← div_eq_inv_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
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
hyz : dist y z = HSub.hSub (α := ℝ) 1 2⁻¹ * dist x z
hyz₁ : dist y z = (1 - 1 / 2) * dist x z
hyz₂ : dist y z = 1 / 2 * dist x z
⊢ dist y z = HSub.hSub (α := ℝ) 1 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) * dist x z
have hyz₃ : dist y z = 2⁻¹ * dist x z
Tactic: rwa [invOf_eq_inv, ← one_div, sub_half, one_div, ← div_eq_inv_mul]
-- 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
E : Type u_3
F : Type u_4
PE : Type u_5
PF : Type u_6
inst_3 : NormedAddCommGroup E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
inst_7 : StrictConvexSpace ℝ E
inst_8 : MetricSpace PE
inst_9 : MetricSpace PF
inst_10 : NormedAddTorsor E PE
inst_11 : NormedAddTorsor F PF
r : ℝ
f : PF → PE
x_1 y_1 z : PE
hi : Isometry f
x y : PF
⊢ f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
have hx : dist (f x) (f (midpoint ℝ x y)) = dist (f x) (f y) / 2
Tactic: apply eq_midpoint_of_dist_eq_half
-- 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
E : Type u_3
F : Type u_4
PE : Type u_5
PF : Type u_6
inst_3 : NormedAddCommGroup E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
inst_7 : StrictConvexSpace ℝ E
inst_8 : MetricSpace PE
inst_9 : MetricSpace PF
inst_10 : NormedAddTorsor E PE
inst_11 : NormedAddTorsor F PF
r : ℝ
f : PF → PE
x_1 y_1 z : PE
hi : Isometry f
x y : PF
hx : dist (f x) (f (midpoint ℝ x y)) = dist (f x) (f y) / 2
⊢ f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
have hy : dist (f (midpoint ℝ x y)) (f y) = dist (f x) (f y) / 2
Tactic: apply eq_midpoint_of_dist_eq_half
-- 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
E : Type u_3
F : Type u_4
PE : Type u_5
PF : Type u_6
inst_3 : NormedAddCommGroup E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
inst_7 : StrictConvexSpace ℝ E
inst_8 : MetricSpace PE
inst_9 : MetricSpace PF
inst_10 : NormedAddTorsor E PE
inst_11 : NormedAddTorsor F PF
r : ℝ
f : PF → PE
x_1 y_1 z : PE
hi : Isometry f
x y : PF
⊢ dist (f x) (f (midpoint ℝ x y)) = dist (f x) (f y) / 2
have hx : dist x (midpoint ℝ x y) = dist x y / 2
Tactic: rw [hi.dist_eq, hi.dist_eq]
-- 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
E : Type u_3
F : Type u_4
PE : Type u_5
PF : Type u_6
inst_3 : NormedAddCommGroup E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
inst_7 : StrictConvexSpace ℝ E
inst_8 : MetricSpace PE
inst_9 : MetricSpace PF
inst_10 : NormedAddTorsor E PE
inst_11 : NormedAddTorsor F PF
r : ℝ
f : PF → PE
x_1 y_1 z : PE
hi : Isometry f
x y : PF
⊢ dist (f (midpoint ℝ x y)) (f y) = dist (f x) (f y) / 2
have hy : dist (midpoint ℝ x y) y = dist x y / 2
Tactic: rw [hi.dist_eq, hi.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : StrictConvexSpace 𝕜 E
x : E
r : ℝ
⊢ StrictConvex 𝕜 (closedBall x r)
have inl : ∀ (hr : r ≤ 0), StrictConvex 𝕜 (closedBall x r)
Tactic: rcases le_or_gt r 0 with hr | hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : StrictConvexSpace 𝕜 E
x : E
r : ℝ
inl : ∀ (hr : r ≤ 0), StrictConvex 𝕜 (closedBall x r)
⊢ StrictConvex 𝕜 (closedBall x r)
have inr : ∀ (hr : 0 < r), StrictConvex 𝕜 (closedBall x r)
Tactic: rcases le_or_gt r 0 with hr | hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (closedBall x r)
have inr : StrictConvex 𝕜 (HVAdd.hVAdd (β := Set E) x (closedBall 0 r))
Tactic: rw [← vadd_closedBall_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ (a : ℝ) (b : ℝ), a + b = 1 ∧ ‖a • x + b • y‖ < 1
⊢ StrictConvexSpace ℝ E
have _ : ∀ (x : E) (hx : Membership.mem (γ := Set E) (closedBall 0 1 \ interior (closedBall 0 1)) x) (y : E)
  (hy : Membership.mem (γ := Set E) (closedBall 0 1 \ interior (closedBall 0 1)) y) (hne : x ≠ y),
  (fun (x y : E) ↦
      ∃ (c : ℝ),
        Membership.mem (α := E) (γ := Set E) (interior (closedBall 0 1)) ((AffineMap.lineMap x y : (a : ℝ) → E) c : E))
    x y
Tactic: refine
    StrictConvexSpace.of_strictConvex_unitClosedBall ℝ
      ((convex_closedBall _ _).strictConvex' fun x hx y hy hne => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ (a : ℝ) (b : ℝ), a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : Membership.mem (γ := Set E) (closedBall 0 1 \ interior (closedBall 0 1)) x
y : E
hy : Membership.mem (γ := Set E) (closedBall 0 1 \ interior (closedBall 0 1)) y
hne : x ≠ y
⊢ (fun (x y : E) ↦
      ∃ (c : ℝ),
        Membership.mem (α := E) (γ := Set E) (interior (closedBall 0 1)) ((AffineMap.lineMap x y : (a : ℝ) → E) c : E))
    x y
have rw : ∀ (hx : ‖x‖ = 1) (y : E) (hy : ‖y‖ = 1) (hne : x ≠ y),
  ∃ (c : ℝ),
    Membership.mem (α := E) (γ := Set E) (interior (closedBall 0 1)) ((AffineMap.lineMap x y : (a : ℝ) → E) c : E)
Tactic: rw [interior_closedBall (0 : E) one_ne_zero, closedBall_diff_ball,
    mem_sphere_zero_iff_norm] at hx hy
Cleared hypotheses: hx, y, hy, hne
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ (a : ℝ) (b : ℝ), a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
⊢ ∃ (c : ℝ),
    Membership.mem (α := E) (γ := Set E) (interior (closedBall 0 1)) ((AffineMap.lineMap x y : (a : ℝ) → E) c : E)
have rcases : ∀ (a b : ℝ) (hab : a + b = 1) (hlt : ‖a • x + b • y‖ < 1),
  ∃ (c : ℝ),
    Membership.mem (α := E) (γ := Set E) (interior (closedBall 0 1)) ((AffineMap.lineMap x y : (a : ℝ) → E) c : E)
Tactic: rcases h x y hx hy hne with ⟨a, b, hab, hlt⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ (a : ℝ) (b : ℝ), a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
a b : ℝ
hab : a + b = 1
hlt : ‖a • x + b • y‖ < 1
⊢ ∃ (c : ℝ),
    Membership.mem (α := E) (γ := Set E) (interior (closedBall 0 1)) ((AffineMap.lineMap x y : (a : ℝ) → E) c : E)
have h₁ : Membership.mem (α := E) (γ := Set E) (interior (closedBall 0 1)) ((AffineMap.lineMap x y : (a : ℝ) → E) b : E)
Tactic: use b
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ (a : ℝ) (b : ℝ), a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
a b : ℝ
hab : a + b = 1
hlt : ‖a • x + b • y‖ < 1
⊢ Membership.mem (α := E) (γ := Set E) (interior (closedBall 0 1)) ((AffineMap.lineMap x y : (a : ℝ) → E) b : E)
have h₁ : Membership.mem (γ := Set E) (interior (closedBall 0 1)) ((1 - b) • x + b • y)
Tactic: rwa [AffineMap.lineMap_apply_module, interior_closedBall (0 : E) one_ne_zero, mem_ball_zero_iff,
    sub_eq_iff_eq_add.2 hab.symm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ (a : ℝ) (b : ℝ), a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
a b : ℝ
hab : a + b = 1
hlt : ‖a • x + b • y‖ < 1
h₁ : Membership.mem (γ := Set E) (interior (closedBall 0 1)) ((1 - b) • x + b • y)
⊢ Membership.mem (α := E) (γ := Set E) (interior (closedBall 0 1)) ((AffineMap.lineMap x y : (a : ℝ) → E) b : E)
have h₂ : Membership.mem (γ := Set E) (ball 0 1) ((1 - b) • x + b • y)
Tactic: rwa [AffineMap.lineMap_apply_module, interior_closedBall (0 : E) one_ne_zero, mem_ball_zero_iff,
    sub_eq_iff_eq_add.2 hab.symm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ (a : ℝ) (b : ℝ), a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
a b : ℝ
hab : a + b = 1
hlt : ‖a • x + b • y‖ < 1
h₁ : Membership.mem (γ := Set E) (interior (closedBall 0 1)) ((1 - b) • x + b • y)
h₂ : Membership.mem (γ := Set E) (ball 0 1) ((1 - b) • x + b • y)
⊢ Membership.mem (α := E) (γ := Set E) (interior (closedBall 0 1)) ((AffineMap.lineMap x y : (a : ℝ) → E) b : E)
have h₃ : ‖(1 - b) • x + b • y‖ < 1
Tactic: rwa [AffineMap.lineMap_apply_module, interior_closedBall (0 : E) one_ne_zero, mem_ball_zero_iff,
    sub_eq_iff_eq_add.2 hab.symm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ (a : ℝ) (b : ℝ), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1
⊢ StrictConvexSpace ℝ E
have refine : Set.Pairwise (closedBall 0 1 \ interior (closedBall 0 1)) fun (x y : E) ↦
  ([x -[ℝ] y] \ frontier (closedBall 0 1)).Nonempty
Tactic: refine StrictConvexSpace.of_strictConvex_unitClosedBall ℝ
    ((convex_closedBall _ _).strictConvex ?_)
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ (a : ℝ) (b : ℝ), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1
⊢ Set.Pairwise (closedBall 0 1 \ interior (closedBall 0 1)) fun (x y : E) ↦
    ([x -[ℝ] y] \ frontier (closedBall 0 1)).Nonempty
have simp : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → x ≠ y → ([x -[ℝ] y] \ sphere 0 1).Nonempty
Tactic: simp only [interior_closedBall _ one_ne_zero, closedBall_diff_ball, Set.Pairwise,
    frontier_closedBall _ one_ne_zero, mem_sphere_zero_iff_norm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ (a : ℝ) (b : ℝ), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
⊢ ([x -[ℝ] y] \ sphere 0 1).Nonempty
have rcases : ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (hne' : ‖a • x + b • y‖ ≠ 1), ([x -[ℝ] y] \ sphere 0 1).Nonempty
Tactic: rcases h x y hx hy hne with ⟨a, b, ha, hb, hab, hne'⟩