-- Mathlib/Analysis/Convex/Segment.lean
lemma segment_inter_eq_endpoint_of_linearIndependent_of_ne [OrderedCommRing 𝕜] [NoZeroDivisors 𝕜]
    [AddCommGroup E] [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}

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedCommRing 𝕜
inst✝² : NoZeroDivisors 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
c : E
hs : -1 * s - t * -1 = 0
⊢ s = t

Tactic:
apply Eq.symm

Result:
case h.h
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedCommRing 𝕜
inst✝² : NoZeroDivisors 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
c : E
hs : -1 * s - t * -1 = 0
⊢ t = s

Proof state:
case h.h
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedCommRing 𝕜
inst✝² : NoZeroDivisors 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
c : E
hs : -1 * s - t * -1 = 0
⊢ t = s

Tactic:
simpa [neg_mul, one_mul, mul_neg, mul_one, sub_neg_eq_add, add_comm _ t,
  ← sub_eq_add_neg, sub_eq_zero] using hs

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedCommRing 𝕜
inst✝² : NoZeroDivisors 𝕜
inst✝¹ : AddCommGroup E
inst✝ : 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)]

Tactic:
simp only [add_sub_add_left_eq_sub]

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedCommRing 𝕜
inst✝² : NoZeroDivisors 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
⊢ LinearIndependent 𝕜 ![t • y - x, s • y - x]

Proof state:
case h.e'_4
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedCommRing 𝕜
inst✝² : NoZeroDivisors 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
H : LinearIndependent 𝕜 ![-1 • x + t • y, -1 • x + s • y]
⊢ ![t • y - x, s • y - x] = ![-1 • x + t • y, -1 • x + s • y]

Tactic:
simp only [neg_smul, one_smul]

Result:
case h.e'_4
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedCommRing 𝕜
inst✝² : NoZeroDivisors 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
H : LinearIndependent 𝕜 ![-1 • x + t • y, -1 • x + s • y]
⊢ ![t • y - x, s • y - x] = ![-x + t • y, -x + s • y]

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedCommRing 𝕜
inst✝² : NoZeroDivisors 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
⊢ -1 * s - t * -1 ≠ 0

Tactic:
contrapose! hs

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedCommRing 𝕜
inst✝² : NoZeroDivisors 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
c : E
hs : -1 * s - t * -1 = 0
⊢ s = t

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedCommRing 𝕜
inst✝² : NoZeroDivisors 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
⊢ 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

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedCommRing 𝕜
inst✝² : NoZeroDivisors 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
⊢ LinearIndependent 𝕜 ![-1 • x + t • y, -1 • x + s • y]

Proof state:
case h.e'_4
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedCommRing 𝕜
inst✝² : NoZeroDivisors 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
H : LinearIndependent 𝕜 ![-1 • x + t • y, -1 • x + s • y]
⊢ ![t • y - x, s • y - x] = ![-x + t • y, -x + s • y]

Tactic:
abel_nf

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedCommRing 𝕜
inst✝² : NoZeroDivisors 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
⊢ LinearIndependent 𝕜 ![-1 • x + t • y, -1 • x + s • y]

Tactic:
apply h.linear_combination_pair_of_det_ne_zero

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedCommRing 𝕜
inst✝² : NoZeroDivisors 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
⊢ -1 * s - t * -1 ≠ 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedCommRing 𝕜
inst✝² : NoZeroDivisors 𝕜
inst✝¹ : AddCommGroup E
inst✝ : 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}

Tactic:
apply segment_inter_eq_endpoint_of_linearIndependent_sub

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedCommRing 𝕜
inst✝² : NoZeroDivisors 𝕜
inst✝¹ : AddCommGroup E
inst✝ : 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)]

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedCommRing 𝕜
inst✝² : NoZeroDivisors 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
H : LinearIndependent 𝕜 ![-1 • x + t • y, -1 • x + s • y]
⊢ LinearIndependent 𝕜 ![t • y - x, s • y - x]

Tactic:
convert H using 1

Result:
case h.e'_4
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedCommRing 𝕜
inst✝² : NoZeroDivisors 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
H : LinearIndependent 𝕜 ![-1 • x + t • y, -1 • x + s • y]
⊢ ![t • y - x, s • y - x] = ![-1 • x + t • y, -1 • x + s • y]