awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
z : E
hzt : z ∈ [c -[𝕜] x]
hzs : z ∈ [c -[𝕜] y]
hzt₁ : ∃ (x_1 : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) x_1 ∧ (1 - x_1) • c + x_1 • x = z
⊢ Membership.mem (γ := Set E) {c} z
have hzs₁ : ∃ (x : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) x ∧ (1 - x) • c + x • y = z
Tactic: rw [segment_eq_image, mem_image] at hzt hzs
Cleared hypotheses: hzt, hzs
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
z : E
hzt : ∃ (x_1 : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) x_1 ∧ (1 - x_1) • c + x_1 • x = z
hzs : ∃ (x : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) x ∧ (1 - x) • c + x • y = z
⊢ Membership.mem (γ := Set E) {c} z
have rcases : ∀ (p : 𝕜) (p0 : 0 ≤ p) (p1 : p ≤ 1)
  (hzs : ∃ (x_1 : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) x_1 ∧ (1 - x_1) • c + x_1 • y = (1 - p) • c + p • x),
  Membership.mem (γ := Set E) {c} ((1 - p) • c + p • x)
Tactic: rcases hzt with ⟨p, ⟨p0, p1⟩, rfl⟩
Cleared hypotheses: z, hzt, hzs
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
hzs : ∃ (x_1 : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) x_1 ∧ (1 - x_1) • c + x_1 • y = (1 - p) • c + p • x
⊢ Membership.mem (γ := Set E) {c} ((1 - p) • c + p • x)
have rcases : ∀ (q : 𝕜) (H : (1 - q) • c + q • y = (1 - p) • c + p • x) (q0 : 0 ≤ q) (q1 : q ≤ 1),
  Membership.mem (γ := Set E) {c} ((1 - p) • c + p • x)
Tactic: rcases hzs with ⟨q, ⟨q0, q1⟩, H⟩
Cleared hypotheses: hzs
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + q • y = (1 - p) • c + p • x
q0 : 0 ≤ q
q1 : q ≤ 1
⊢ Membership.mem (γ := Set E) {c} ((1 - p) • c + p • x)
have Hx : x = x - c + c
Tactic: have Hx : x = (x - c) + c := by abel
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + q • y = (1 - p) • c + p • x
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
⊢ Membership.mem (γ := Set E) {c} ((1 - p) • c + p • x)
have Hy : y = y - c + c
Tactic: have Hy : y = (y - c) + c := by abel
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + q • y = (1 - p) • c + p • x
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
Hy : y = y - c + c
⊢ Membership.mem (γ := Set E) {c} ((1 - p) • c + p • x)
have H₁ : (1 - q) • c + (q • (y - c) + q • c) = (1 - p) • c + (p • (x - c) + p • c)
Tactic: rw [Hx, Hy, smul_add, smul_add] at H
Cleared hypotheses: H, q0, q1, Hx, Hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + (q • (y - c) + q • c) = (1 - p) • c + (p • (x - c) + p • c)
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
Hy : y = y - c + c
⊢ c + q • (y - c) = c + p • (x - c)
have h₁ : c + q • (y - c) = (1 - q) • c + (q • (y - c) + q • c)
Tactic: convert! H using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + (q • (y - c) + q • c) = (1 - p) • c + (p • (x - c) + p • c)
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
Hy : y = y - c + c
h₁ : c + q • (y - c) = (1 - q) • c + (q • (y - c) + q • c)
⊢ c + q • (y - c) = c + p • (x - c)
have h₂ : c + p • (x - c) = (1 - p) • c + (p • (x - c) + p • c)
Tactic: convert! H using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + (q • (y - c) + q • c) = (1 - p) • c + (p • (x - c) + p • c)
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
Hy : y = y - c + c
⊢ Membership.mem (γ := Set E) {c} ((1 - p) • c + p • x)
have this : c + q • (y - c) = c + p • (x - c)
Tactic: have : c + q • (y - c) = c + p • (x - c) := by
    convert! H using 1 <;> simp [sub_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + (q • (y - c) + q • c) = (1 - p) • c + (p • (x - c) + p • c)
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
Hy : y = y - c + c
this : c + q • (y - c) = c + p • (x - c)
⊢ Membership.mem (γ := Set E) {c} ((1 - p) • c + p • x)
have obtain : ∀ (p0 : LE.le.{u_1} (α := 𝕜) 0 0) (p1 : LE.le.{u_1} (α := 𝕜) 0 1) (q0 : LE.le.{u_1} (α := 𝕜) 0 0)
  (q1 : LE.le.{u_1} (α := 𝕜) 0 1)
  (H :
    HSub.hSub (α := 𝕜) 1 0 • c +
        (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (y - c) + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 c) =
      HSub.hSub (α := 𝕜) 1 0 • c +
        (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (x - c) + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 c))
  (this : c + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (y - c) = c + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (x - c)),
  Membership.mem (γ := Set E) {c} (HSub.hSub (α := 𝕜) 1 0 • c + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)
Tactic: obtain ⟨rfl, rfl⟩ : p = 0 ∧ q = 0 := h.eq_zero_of_pair' ((add_right_inj c).1 this).symm
Cleared hypotheses: p, p0, p1, q, H, q0, q1, this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : ZeroLEOneClass 𝕜
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
⊢ [c -[𝕜] x] ∩ [c -[𝕜] y] = {c}
have refine : {c} ⊆ [c -[𝕜] x] ∩ [c -[𝕜] y]
Tactic: refine (segment_inter_subset_endpoint_of_linearIndependent_sub 𝕜 h).antisymm ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommRing 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y z : E
h : x ∈ [y -[𝕜] z]
⊢ SameRay 𝕜 (x - y) (z - x)
have h₁ : Membership.mem (γ := Set E) ((fun (θ : 𝕜) ↦ y + θ • (z - y)) '' Icc 0 1) x
Tactic: rw [segment_eq_image'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommRing 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y z : E
h : Membership.mem (γ := Set E) ((fun (θ : 𝕜) ↦ y + θ • (z - y)) '' Icc 0 1) x
⊢ SameRay 𝕜 (x - y) (z - x)
have rcases : ∀ (θ : 𝕜) (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1),
  SameRay 𝕜 ((fun (θ : 𝕜) ↦ y + θ • (z - y)) θ - y) (z - (fun (θ : 𝕜) ↦ y + θ • (z - y)) θ)
Tactic: rcases h with ⟨θ, ⟨hθ₀, hθ₁⟩, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommRing 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : IsDomain 𝕜
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
⊢ [c + x -[𝕜] c + t • y] ∩ [c + x -[𝕜] c + s • y] = {c + x}
have h₁ : LinearIndependent 𝕜 ![c + t • y - (c + x), c + s • y - (c + x)]
Tactic: apply segment_inter_eq_endpoint_of_linearIndependent_sub
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommRing 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : IsDomain 𝕜
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
⊢ LinearIndependent 𝕜 ![c + t • y - (c + x), c + s • y - (c + x)]
have h₁ : LinearIndependent 𝕜 ![t • y - x, s • y - x]
Tactic: simp only [add_sub_add_left_eq_sub]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommRing 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : IsDomain 𝕜
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
H :
  LinearIndependent 𝕜
    ![HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-1) x + t • y, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-1) x + s • y]
⊢ LinearIndependent 𝕜 ![t • y - x, s • y - x]
have h₁ : ![t • y - x, s • y - x] =
  ![HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-1) x + t • y, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-1) x + s • y]
Tactic: convert! H using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommRing 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : IsDomain 𝕜
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
H :
  LinearIndependent 𝕜
    ![HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-1) x + t • y, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-1) x + s • y]
⊢ ![t • y - x, s • y - x] =
    ![HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-1) x + t • y, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-1) x + s • y]
have h₁ : ![t • y - x, s • y - x] = ![-x + t • y, -x + s • y]
Tactic: simp only [neg_smul, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommRing 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : IsDomain 𝕜
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
⊢ LinearIndependent 𝕜 ![t • y - x, s • y - x]
have h₁ : LinearIndependent 𝕜
  ![HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-1) x + t • y, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-1) x + s • y]
Tactic: suffices H : LinearIndependent 𝕜 ![(-1 : 𝕜) • x + t • y, (-1 : 𝕜) • x + s • y] by
    convert! H using 1; simp only [neg_smul, one_smul]; abel_nf
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommRing 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : IsDomain 𝕜
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
⊢ LinearIndependent 𝕜
    ![HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-1) x + t • y, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-1) x + s • y]
have inst : Nontrivial 𝕜
Tactic: nontriviality 𝕜
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommRing 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : IsDomain 𝕜
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
inst_6 : Nontrivial 𝕜
⊢ LinearIndependent 𝕜
    ![HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-1) x + t • y, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-1) x + s • y]
have h₁ : LinearIndependent 𝕜 ![x, y] ∧ -1 * s ≠ t * -1
Tactic: rw [LinearIndependent.pair_add_smul_add_smul_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : Invertible (α := 𝕜) 2
x y : E
⊢ midpoint 𝕜 x y ∈ openSegment 𝕜 x y
have rw : Membership.mem (γ := Set E) (image.{u_1, u_2} (α := 𝕜) (⇑(AffineMap.lineMap x y) : (a : 𝕜) → E) (Ioo 0 1))
  (midpoint 𝕜 x y)
Tactic: rw [openSegment_eq_image_lineMap]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : Invertible (α := 𝕜) 2
x y : E
⊢ x ∈ openSegment 𝕜 (x - y) (x + y)
have h : x = midpoint 𝕜 (x - y) (x + y)
Tactic: convert! midpoint_mem_openSegment (𝕜 := 𝕜) (x - y) (x + y)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : Invertible (α := 𝕜) 2
x y : E
⊢ x = midpoint 𝕜 (x - y) (x + y)
have h : x = x
Tactic: rw [midpoint_sub_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : Invertible (α := 𝕜) 2
x y : E
⊢ x ∈ openSegment 𝕜 (x + y) (x - y)
have h : x = midpoint 𝕜 (x + y) (x - y)
Tactic: convert! midpoint_mem_openSegment (𝕜 := 𝕜) (x + y) (x - y)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : Invertible (α := 𝕜) 2
x y : E
⊢ x = midpoint 𝕜 (x + y) (x - y)
have h : x = x
Tactic: rw [midpoint_add_sub]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
⊢ x ∈ openSegment 𝕜 x y ↔ x = y
have mp : x ∈ openSegment 𝕜 x y → x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
mp : x ∈ openSegment 𝕜 x y → x = y
⊢ x ∈ openSegment 𝕜 x y ↔ x = y
have mpr : x = y → x ∈ openSegment 𝕜 x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
a b : 𝕜
left : 0 < a
hb : 0 < b
hab : a + b = 1
hx : a • x + b • y = x
⊢ x = y
have mp : a • x + (fun (x : E) ↦ b • x) x = a • x + (fun (x : E) ↦ b • x) y
Tactic: refine smul_right_injective _ hb.ne' ((add_right_inj (a • x)).1 ?_)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
a b : 𝕜
left : 0 < a
hb : 0 < b
hab : a + b = 1
hx : a • x + b • y = x
⊢ a • x + (fun (x : E) ↦ b • x) x = a • x + (fun (x : E) ↦ b • x) y
have mp : a • x + (fun (x : E) ↦ b • x) x = x
Tactic: rw [hx, ← add_smul, hab, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
a b : 𝕜
left : 0 < a
hb : 0 < b
hab : a + b = 1
hx : a • x + b • y = x
mp : a • x + (fun (x : E) ↦ b • x) x = x
⊢ a • x + (fun (x : E) ↦ b • x) x = a • x + (fun (x : E) ↦ b • x) y
have mp₁ : (a + b) • x = x
Tactic: rw [hx, ← add_smul, hab, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
a b : 𝕜
left : 0 < a
hb : 0 < b
hab : a + b = 1
hx : a • x + b • y = x
mp : a • x + (fun (x : E) ↦ b • x) x = x
mp₁ : (a + b) • x = x
⊢ a • x + (fun (x : E) ↦ b • x) x = a • x + (fun (x : E) ↦ b • x) y
have mp₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x = x
Tactic: rw [hx, ← add_smul, hab, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
a b : 𝕜
left : 0 < a
hb : 0 < b
hab : a + b = 1
hx : a • x + b • y = x
mp : a • x + (fun (x : E) ↦ b • x) x = x
mp₁ : (a + b) • x = x
mp₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x = x
⊢ a • x + (fun (x : E) ↦ b • x) x = a • x + (fun (x : E) ↦ b • x) y
have mp₃ : x = x
Tactic: rw [hx, ← add_smul, hab, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
⊢ x ∈ openSegment 𝕜 x x
have mpr : Membership.mem (γ := Set E) {x} x
Tactic: rw [openSegment_same]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
⊢ y ∈ openSegment 𝕜 x y ↔ x = y
have rw : y ∈ openSegment 𝕜 y x ↔ x = y
Tactic: rw [openSegment_symm, left_mem_openSegment_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
rw : y ∈ openSegment 𝕜 y x ↔ x = y
⊢ y ∈ openSegment 𝕜 x y ↔ x = y
have rw₁ : y = x ↔ x = y
Tactic: rw [openSegment_symm, left_mem_openSegment_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
rw : y ∈ openSegment 𝕜 y x ↔ x = y
rw₁ : y = x ↔ x = y
⊢ y ∈ openSegment 𝕜 x y ↔ x = y
have rw₂ : x = y ↔ x = y
Tactic: rw [openSegment_symm, left_mem_openSegment_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y z : E
⊢ x ∈ [y -[𝕜] z] ↔ ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
have mp : x ∈ [y -[𝕜] z] → ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y z : E
mp : x ∈ [y -[𝕜] z] → ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
⊢ x ∈ [y -[𝕜] z] ↔ ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
have mpr : (∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x) → x ∈ [y -[𝕜] z]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ (a_1 : 𝕜) (b_1 : 𝕜),
    0 ≤ a_1 ∧ 0 ≤ b_1 ∧ 0 < a_1 + b_1 ∧ (a_1 / (a_1 + b_1)) • y + (b_1 / (a_1 + b_1)) • z = a • y + b • z
have right : 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = a • y + b • z
Tactic: use a, b, ha, hb
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ (a / (a + b)) • y + (b / (a + b)) • z ∈ [y -[𝕜] z]
have mpr : a / (a + b) + b / (a + b) = 1
Tactic: refine ⟨a / (a + b), b / (a + b), by positivity, by positivity, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ a / (a + b) + b / (a + b) = 1
have mpr : (a + b) / (a + b) = 1
Tactic: rw [← add_div, div_self hab.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
mpr : (a + b) / (a + b) = 1
⊢ a / (a + b) + b / (a + b) = 1
have mpr₁ : Eq.{u_1 + 1} (α := 𝕜) 1 1
Tactic: rw [← add_div, div_self hab.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y z : E
⊢ x ∈ openSegment 𝕜 y z ↔ ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
have mp : x ∈ openSegment 𝕜 y z → ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y z : E
mp : x ∈ openSegment 𝕜 y z → ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
⊢ x ∈ openSegment 𝕜 y z ↔ ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
have mpr : (∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x) → x ∈ openSegment 𝕜 y z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ∃ (a_1 : 𝕜) (b_1 : 𝕜), 0 < a_1 ∧ 0 < b_1 ∧ (a_1 / (a_1 + b_1)) • y + (b_1 / (a_1 + b_1)) • z = a • y + b • z
have right : (a / (a + b)) • y + (b / (a + b)) • z = a • y + b • z
Tactic: use a, b, ha, hb
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (a / (a + b)) • y + (b / (a + b)) • z = a • y + b • z
have right : (a / 1) • y + (b / 1) • z = a • y + b • z
Tactic: rw [hab, div_one, div_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Segment (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
right : (a / 1) • y + (b / 1) • z = a • y + b • z
⊢ (a / (a + b)) • y + (b / (a + b)) • z = a • y + b • z
have right₁ : a • y + (b / 1) • z = a • y + b • z
Tactic: rw [hab, div_one, div_one]