awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Segment
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
⊢ (1 - q) • c + (q • (y - c) + q • c) = (1 - p) • c + (p • (x - c) + p • c)

Tactic:
H
-- Module: Mathlib.Analysis.Convex.Segment
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)
h₂ : c + p • (x - c) = (1 - p) • c + (p • (x - c) + p • c)
⊢ c + q • (y - c) = c + p • (x - c)

Tactic:
convert! H using 1
-- Module: Mathlib.Analysis.Convex.Segment
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) = (1 - q) • c + (q • (y - c) + q • c)

Tactic:
simp [sub_smul]

Premises used: sub_smul
-- Module: Mathlib.Analysis.Convex.Segment
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 + p • (x - c) = (1 - p) • c + (p • (x - c) + p • c)

Tactic:
simp [sub_smul]

Premises used: sub_smul
-- Module: Mathlib.Analysis.Convex.Segment
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)

Tactic:
have : c + q • (y - c) = c + p • (x - c) := by
    convert! H using 1 <;> simp [sub_smul]
-- Module: Mathlib.Analysis.Convex.Segment
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)
⊢ p = 0 ∧ q = 0

Tactic:
h.eq_zero_of_pair' ((add_right_inj c).1 this).symm

Premises used: LinearIndependent.eq_zero_of_pair', Iff.mp, Eq.symm, add_right_inj
-- Module: Mathlib.Analysis.Convex.Segment
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)
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)
⊢ Membership.mem (γ := Set E) {c} ((1 - p) • c + p • x)

Tactic:
obtain ⟨rfl, rfl⟩ : p = 0 ∧ q = 0 := h.eq_zero_of_pair' ((add_right_inj c).1 this).symm

Premises used: LinearIndependent.eq_zero_of_pair', Iff.mp, Eq.symm, add_right_inj, rfl
-- Module: Mathlib.Analysis.Convex.Segment
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]
Hx : x = x - c + c
Hy : y = y - c + c
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:
simp
-- Module: Mathlib.Analysis.Convex.Segment
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}

Tactic:
(segment_inter_subset_endpoint_of_linearIndependent_sub 𝕜 h).antisymm ?_

Premises used: segment_inter_subset_endpoint_of_linearIndependent_sub, HasSubset.Subset.antisymm
-- Module: Mathlib.Analysis.Convex.Segment
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]
refine : {c} ⊆ [c -[𝕜] x] ∩ [c -[𝕜] y]
⊢ [c -[𝕜] x] ∩ [c -[𝕜] y] = {c}

Tactic:
refine (segment_inter_subset_endpoint_of_linearIndependent_sub 𝕜 h).antisymm ?_

Premises used: segment_inter_subset_endpoint_of_linearIndependent_sub, HasSubset.Subset.antisymm
-- Module: Mathlib.Analysis.Convex.Segment
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} ⊆ [c -[𝕜] x] ∩ [c -[𝕜] y]

Tactic:
simp [singleton_subset_iff, left_mem_segment]

Premises used: Set.singleton_subset_iff, left_mem_segment
-- Module: Mathlib.Analysis.Convex.Segment
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]
⊢ Membership.mem (γ := Set E) ((fun (θ : 𝕜) ↦ y + θ • (z - y)) '' Icc 0 1) x

Tactic:
rw [segment_eq_image'] at h

Premises used: segment_eq_image'
-- Module: Mathlib.Analysis.Convex.Segment
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
rcases :
  ∀ (θ : 𝕜) (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1),
    SameRay 𝕜 ((fun (θ : 𝕜) ↦ y + θ • (z - y)) θ - y) (z - (fun (θ : 𝕜) ↦ y + θ • (z - y)) θ)
⊢ SameRay 𝕜 (x - y) (z - x)

Tactic:
rcases h with ⟨θ, ⟨hθ₀, hθ₁⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommRing 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
y z : E
θ : 𝕜
hθ₀ : 0 ≤ θ
hθ₁ : θ ≤ 1
⊢ SameRay 𝕜 ((fun (θ : 𝕜) ↦ y + θ • (z - y)) θ - y) (z - (fun (θ : 𝕜) ↦ y + θ • (z - y)) θ)

Tactic:
simpa only [add_sub_cancel_left, ← sub_sub, sub_smul, one_smul] using
    (SameRay.sameRay_nonneg_smul_left (z - y) hθ₀).nonneg_smul_right (sub_nonneg.2 hθ₁)

Premises used: Iff.mpr, add_sub_cancel_left, SameRay.nonneg_smul_right, HSub.hSub, SameRay.sameRay_nonneg_smul_left, sub_smul, one_smul, sub_sub, sub_nonneg
-- Module: Mathlib.Analysis.Convex.Segment
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 𝕜 ![c + t • y - (c + x), c + s • y - (c + x)]
⊢ [c + x -[𝕜] c + t • y] ∩ [c + x -[𝕜] c + s • y] = {c + x}

Tactic:
apply segment_inter_eq_endpoint_of_linearIndependent_sub

Premises used: segment_inter_eq_endpoint_of_linearIndependent_sub
-- Module: Mathlib.Analysis.Convex.Segment
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 𝕜 ![t • y - x, s • y - x]
⊢ LinearIndependent 𝕜 ![c + t • y - (c + x), c + s • y - (c + x)]

Tactic:
simp only [add_sub_add_left_eq_sub]

Premises used: add_sub_add_left_eq_sub
-- Module: Mathlib.Analysis.Convex.Segment
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 𝕜
    ![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:
H
-- Module: Mathlib.Analysis.Convex.Segment
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]
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]
⊢ LinearIndependent 𝕜 ![t • y - x, s • y - x]

Tactic:
convert! H using 1
-- Module: Mathlib.Analysis.Convex.Segment
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]
h₁ : ![t • y - x, s • y - x] = ![-x + t • y, -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]

Tactic:
simp only [neg_smul, one_smul]

Premises used: neg_smul, one_smul
-- Module: Mathlib.Analysis.Convex.Segment
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] = ![-x + t • y, -x + s • y]

Tactic:
abel_nf
-- Module: Mathlib.Analysis.Convex.Segment
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]

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
-- Module: Mathlib.Analysis.Convex.Segment
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
⊢ Nontrivial 𝕜

Tactic:
nontriviality 𝕜
-- Module: Mathlib.Analysis.Convex.Segment
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 𝕜
h₁ : LinearIndependent 𝕜 ![x, y] ∧ -1 * s ≠ t * -1
⊢ 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:
rw [LinearIndependent.pair_add_smul_add_smul_iff]

Premises used: LinearIndependent.pair_add_smul_add_smul_iff
-- Module: Mathlib.Analysis.Convex.Segment
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 𝕜 ![x, y] ∧ -1 * s ≠ t * -1

Tactic:
aesop
-- Module: Mathlib.Analysis.Convex.Segment
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
rw :
  Membership.mem (γ := Set E) (image.{u_1, u_2} (α := 𝕜) (⇑(AffineMap.lineMap x y) : (a : 𝕜) → E) (Ioo 0 1))
    (midpoint 𝕜 x y)
⊢ midpoint 𝕜 x y ∈ openSegment 𝕜 x y

Tactic:
rw [openSegment_eq_image_lineMap]

Premises used: openSegment_eq_image_lineMap
-- Module: Mathlib.Analysis.Convex.Segment
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
⊢ Membership.mem (γ := Set E) (image.{u_1, u_2} (α := 𝕜) (⇑(AffineMap.lineMap x y) : (a : 𝕜) → E) (Ioo 0 1))
    (midpoint 𝕜 x y)

Tactic:
⟨⅟2, ⟨invOf_pos.mpr two_pos, invOf_lt_one one_lt_two⟩, rfl⟩

Premises used: Iff.mpr, invOf_pos, Set.Mem, setOf, Invertible.invOf, two_pos, invOf_lt_one, And.intro, Exists.intro, one_lt_two, Set.image, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Convex.Segment
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
⊢ Membership.mem (γ := Set E) (image.{u_1, u_2} (α := 𝕜) (⇑(AffineMap.lineMap x y) : (a : 𝕜) → E) (Ioo 0 1))
    (midpoint 𝕜 x y)

Tactic:
exact ⟨⅟2, ⟨invOf_pos.mpr two_pos, invOf_lt_one one_lt_two⟩, rfl⟩
-- Module: Mathlib.Analysis.Convex.Segment
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 ∈ [x -[𝕜] y]

Tactic:
openSegment_subset_segment _ _ _ <| midpoint_mem_openSegment _ _

Premises used: midpoint_mem_openSegment, openSegment_subset_segment
-- Module: Mathlib.Analysis.Convex.Segment
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) (x + y) ∈ openSegment 𝕜 (x - y) (x + y)

Tactic:
midpoint_mem_openSegment (𝕜 := 𝕜) (x - y) (x + y)

Premises used: HSub.hSub, midpoint_mem_openSegment, HAdd.hAdd
-- Module: Mathlib.Analysis.Convex.Segment
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
h : x = midpoint 𝕜 (x - y) (x + y)
⊢ x ∈ openSegment 𝕜 (x - y) (x + y)

Tactic:
convert! midpoint_mem_openSegment (𝕜 := 𝕜) (x - y) (x + y)

Premises used: HSub.hSub, midpoint_mem_openSegment, HAdd.hAdd
-- Module: Mathlib.Analysis.Convex.Segment
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
h h₁ : x = x
⊢ x = midpoint 𝕜 (x - y) (x + y)

Tactic:
rw [midpoint_sub_add]

Premises used: midpoint_sub_add
-- Module: Mathlib.Analysis.Convex.Segment
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 ∈ [x - y -[𝕜] x + y]

Tactic:
openSegment_subset_segment _ _ _ <| mem_openSegment_sub_add _ _

Premises used: mem_openSegment_sub_add, openSegment_subset_segment
-- Module: Mathlib.Analysis.Convex.Segment
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) (x - y) ∈ openSegment 𝕜 (x + y) (x - y)

Tactic:
midpoint_mem_openSegment (𝕜 := 𝕜) (x + y) (x - y)

Premises used: HSub.hSub, midpoint_mem_openSegment, HAdd.hAdd
-- Module: Mathlib.Analysis.Convex.Segment
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
h : x = midpoint 𝕜 (x + y) (x - y)
⊢ x ∈ openSegment 𝕜 (x + y) (x - y)

Tactic:
convert! midpoint_mem_openSegment (𝕜 := 𝕜) (x + y) (x - y)

Premises used: HSub.hSub, midpoint_mem_openSegment, HAdd.hAdd
-- Module: Mathlib.Analysis.Convex.Segment
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
h h₁ : x = x
⊢ x = midpoint 𝕜 (x + y) (x - y)

Tactic:
rw [midpoint_add_sub]

Premises used: midpoint_add_sub
-- Module: Mathlib.Analysis.Convex.Segment
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 ∈ [x + y -[𝕜] x - y]

Tactic:
openSegment_subset_segment _ _ _ <| mem_openSegment_add_sub _ _

Premises used: mem_openSegment_add_sub, openSegment_subset_segment
-- Module: Mathlib.Analysis.Convex.Segment
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
mpr : x = y → x ∈ openSegment 𝕜 x y
⊢ x ∈ openSegment 𝕜 x y ↔ x = y

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Segment
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

Tactic:
smul_right_injective _ hb.ne' ((add_right_inj (a • x)).1 ?_)

Premises used: smul_right_injective, LT.lt.ne', Iff.mp, HSMul.hSMul, add_right_inj
-- Module: Mathlib.Analysis.Convex.Segment
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 = a • x + (fun (x : E) ↦ b • x) y
⊢ x = y

Tactic:
refine smul_right_injective _ hb.ne' ((add_right_inj (a • x)).1 ?_)

Premises used: smul_right_injective, LT.lt.ne', Iff.mp, HSMul.hSMul, add_right_inj
-- Module: Mathlib.Analysis.Convex.Segment
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
mp₃ mp₄ : x = x
⊢ a • x + (fun (x : E) ↦ b • x) x = a • x + (fun (x : E) ↦ b • x) y

Tactic:
rw [hx, ← add_smul, hab, one_smul]

Premises used: one_smul, add_smul
-- Module: Mathlib.Analysis.Convex.Segment
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
mpr : Membership.mem (γ := Set E) {x} x
⊢ x ∈ openSegment 𝕜 x x

Tactic:
rw [openSegment_same]

Premises used: openSegment_same
-- Module: Mathlib.Analysis.Convex.Segment
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
⊢ Membership.mem (γ := Set E) {x} x

Tactic:
mem_singleton _

Premises used: Set.mem_singleton
-- Module: Mathlib.Analysis.Convex.Segment
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
⊢ Membership.mem (γ := Set E) {x} x

Tactic:
exact mem_singleton _

Premises used: Set.mem_singleton
-- Module: Mathlib.Analysis.Convex.Segment
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
rw₂ rw₃ : x = y ↔ x = y
⊢ y ∈ openSegment 𝕜 x y ↔ x = y

Tactic:
rw [openSegment_symm, left_mem_openSegment_iff, eq_comm]

Premises used: eq_comm, openSegment_symm, left_mem_openSegment_iff
-- Module: Mathlib.Analysis.Convex.Segment
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
mpr : (∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x) → x ∈ [y -[𝕜] z]
⊢ x ∈ [y -[𝕜] z] ↔ ∃ (a : 𝕜) (b : 𝕜), 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Segment
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 : 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = a • y + b • z
⊢ ∃ (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

Tactic:
use a, b, ha, hb
-- Module: Mathlib.Analysis.Convex.Segment
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
⊢ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = a • y + b • z

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Convex.Segment
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
⊢ 0 ≤ a / (a + b)

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Segment
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
⊢ 0 ≤ b / (a + b)

Tactic:
positivity