awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
inst_3 : Archimedean α
hδ : 0 < δ
m : ℕ
hm : b - a ≤ m • δ
n : ℕ
hn : n ≥ m
rw : b ≤ n • δ + a
⊢ (↑(addNSMul h δ n) : α) = b

Tactic:
rw [addNSMul, coe_projIcc, add_comm, min_eq_left_iff.mpr, max_eq_right h]

Premises used: Iff.mpr, Set.coe_projIcc, Set.Icc.addNSMul, add_comm, max_eq_right, min_eq_left_iff
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
inst_3 : Archimedean α
hδ : 0 < δ
m : ℕ
hm : b - a ≤ m • δ
n : ℕ
hn : n ≥ m
⊢ b ≤ n • δ + a

Tactic:
sub_le_iff_le_add.mp (hm.trans <| nsmul_le_nsmul_left hδ.le hn)

Premises used: sub_le_iff_le_add, LT.lt.le, nsmul_le_nsmul_left, Iff.mp, LE.le.trans
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
inst_3 : Archimedean α
hδ : 0 < δ
m : ℕ
hm : b - a ≤ m • δ
n : ℕ
hn : n ≥ m
⊢ b ≤ n • δ + a

Tactic:
exact sub_le_iff_le_add.mp (hm.trans <| nsmul_le_nsmul_left hδ.le hn)

Premises used: sub_le_iff_le_add, LT.lt.le, nsmul_le_nsmul_left, Iff.mp, LE.le.trans
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
hδ : 0 ≤ δ
⊢ Monotone (addNSMul h δ)

Tactic:
fun _ _ hnm ↦ monotone_projIcc h <| (add_le_add_iff_left _).mpr (nsmul_le_nsmul_left hδ hnm)

Premises used: Iff.mpr, Monotone, add_le_add_iff_left, nsmul_le_nsmul_left, Set.monotone_projIcc
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
hδ : 0 ≤ δ
t : (↑(Icc a b) : Type u_1)
n : ℕ
ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))
h₁ : (↑t : α) ≤ (↑(projIcc a b h (a + (n + 1) • δ)) : α)
⊢ (↑t : α) - (↑(addNSMul h δ n) : α) ≤ (↑(projIcc a b h (a + (n + 1) • δ)) : α) - (↑(addNSMul h δ n) : α)

Tactic:
apply sub_le_sub_right

Premises used: sub_le_sub_right
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
hδ : 0 ≤ δ
t : (↑(Icc a b) : Type u_1)
n : ℕ
ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))
⊢ (↑t : α) ≤ (↑(projIcc a b h (a + (n + 1) • δ)) : α)

Tactic:
ht.2

Premises used: And.right
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
hδ : 0 ≤ δ
t : (↑(Icc a b) : Type u_1)
n : ℕ
ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))
⊢ (↑t : α) ≤ (↑(projIcc a b h (a + (n + 1) • δ)) : α)

Tactic:
exact ht.2

Premises used: And.right
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
hδ : 0 ≤ δ
t : (↑(Icc a b) : Type u_1)
n : ℕ
ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))
rw : |δ| ≤ δ
⊢ |a + (n + 1) • δ - (a + n • δ)| ≤ δ

Tactic:
rw [add_sub_add_comm, sub_self, zero_add, succ_nsmul', add_sub_cancel_right]

Premises used: sub_self, zero_add, succ_nsmul', add_sub_add_comm, add_sub_cancel_right
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
hδ : 0 ≤ δ
t : (↑(Icc a b) : Type u_1)
n : ℕ
ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))
⊢ |δ| ≤ δ

Tactic:
(abs_eq_self.mpr hδ).le

Premises used: Iff.mpr, Eq.le, abs_eq_self
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
hδ : 0 ≤ δ
t : (↑(Icc a b) : Type u_1)
n : ℕ
ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))
⊢ |δ| ≤ δ

Tactic:
exact (abs_eq_self.mpr hδ).le

Premises used: Iff.mpr, Eq.le, abs_eq_self
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type ?u.80119
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a_1 b_1 c d : α
h : a_1 ≤ b_1
δ : α
a b : ℝ
x y : (↑(Icc a b) : Type)
t : (↑unitInterval : Type)
left : a ≤ (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ)
right : (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) ≤ b
⊢ (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) ∈ Icc a b

Tactic:
constructor
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type ?u.80119
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a_1 b_1 c d : α
h : a_1 ≤ b_1
δ : α
a b : ℝ
x y : (↑(Icc a b) : Type)
t : (↑unitInterval : Type)
nlinarith :
  (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) < a →
    (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) - a + (0 - (a - (↑x : ℝ)) * ((↑t : ℝ) - 1)) +
        (0 - (a - (↑y : ℝ)) * (0 - (↑t : ℝ))) =
      0
⊢ a ≤ (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ)

Tactic:
nlinarith [x.2.1, y.2.1, t.2.1, t.2.2]

Premises used: And.right, And.left, Subtype.property
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type ?u.80119
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a_1 b_1 c d : α
h : a_1 ≤ b_1
δ : α
a b : ℝ
x y : (↑(Icc a b) : Type)
t : (↑unitInterval : Type)
nlinarith :
  b < (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) →
    b - ((1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ)) + (0 - ((↑x : ℝ) - b) * ((↑t : ℝ) - 1)) +
        (0 - ((↑y : ℝ) - b) * (0 - (↑t : ℝ))) =
      0
⊢ (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) ≤ b

Tactic:
nlinarith [x.2.2, y.2.2, t.2.1, t.2.2]

Premises used: And.right, And.left, Subtype.property
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y : (↑(Icc a b) : Type)
t : (↑unitInterval : Type)
⊢ (↑(convexComb x y t) : ℝ) = (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y : (↑(Icc a b) : Type)
⊢ convexComb x y 0 = x

Tactic:
simp [convexComb]

Premises used: Set.Icc.convexComb
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y : (↑(Icc a b) : Type)
⊢ convexComb x y 1 = y

Tactic:
simp [convexComb]

Premises used: Set.Icc.convexComb
-- Module: Mathlib.Topology.UnitInterval
Goal:
t : (↑unitInterval : Type)
⊢ convexComb 0 1 t = t

Tactic:
simp [convexComb]

Premises used: Set.Icc.convexComb
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x : (↑(Icc a b) : Type)
t : (↑unitInterval : Type)
⊢ convexComb x x t = x

Tactic:
simp [convexComb, sub_mul]

Premises used: Set.Icc.convexComb, sub_mul
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y : (↑(Icc a b) : Type)
t : (↑unitInterval : Type)
simp : (↑t : ℝ) * (↑x : ℝ) + (1 - (↑t : ℝ)) * (↑y : ℝ) = (1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑x : ℝ)
⊢ convexComb x y (unitInterval.symm t) = convexComb y x t

Tactic:
simp [convexComb]

Premises used: Set.Icc.convexComb
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y : (↑(Icc a b) : Type)
t : (↑unitInterval : Type)
⊢ (↑t : ℝ) * (↑x : ℝ) + (1 - (↑t : ℝ)) * (↑y : ℝ) = (1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑x : ℝ)

Tactic:
abel
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y : (↑(Icc a b) : Type)
h : x ≤ y
t : (↑unitInterval : Type)
rw : ∀ (h : (↑x : ℝ) ≤ (↑y : ℝ)) (t : (↑unitInterval : Type)), (↑x : ℝ) ≤ (↑(convexComb x y t) : ℝ)
⊢ x ≤ convexComb x y t

Tactic:
rw [← Subtype.coe_le_coe] at h ⊢

Premises used: Subtype.coe_le_coe
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y : (↑(Icc a b) : Type)
h : (↑x : ℝ) ≤ (↑y : ℝ)
t : (↑unitInterval : Type)
nlinarith :
  (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) < (↑x : ℝ) →
    (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) - (↑x : ℝ) + (0 - ((↑x : ℝ) - (↑y : ℝ)) * (0 - (↑t : ℝ))) = 0
⊢ (↑x : ℝ) ≤ (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ)

Tactic:
nlinarith [t.2.1, t.2.2]

Premises used: And.right, And.left, Subtype.property
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y : (↑(Icc a b) : Type)
h : x ≤ y
t : (↑unitInterval : Type)
rw : ∀ (h : (↑x : ℝ) ≤ (↑y : ℝ)) (t : (↑unitInterval : Type)), (↑(convexComb x y t) : ℝ) ≤ (↑y : ℝ)
⊢ convexComb x y t ≤ y

Tactic:
rw [← Subtype.coe_le_coe] at h ⊢

Premises used: Subtype.coe_le_coe
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y : (↑(Icc a b) : Type)
h : (↑x : ℝ) ≤ (↑y : ℝ)
t : (↑unitInterval : Type)
nlinarith :
  (↑y : ℝ) < (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) →
    (↑y : ℝ) - ((1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ)) + (0 - ((↑x : ℝ) - (↑y : ℝ)) * ((↑t : ℝ) - 1)) = 0
⊢ (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) ≤ (↑y : ℝ)

Tactic:
nlinarith [t.2.1, t.2.2]

Premises used: And.right, And.left, Subtype.property
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y : (↑(Icc a b) : Type)
⊢ Continuous (Y := (↑(Icc a b) : Type)) fun (t : (↑unitInterval : Type)) ↦
    Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc a b) ((1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ)) ⋯

Tactic:
fun_prop
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
⊢ Continuous (Y := (↑(Icc a b) : Type)) fun (x : (↑(Icc a b) : Type) × (↑(Icc a b) : Type) × (↑unitInterval : Type)) ↦
    Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc a b) ((1 - (↑x.2.2 : ℝ)) * (↑x.1 : ℝ) + (↑x.2.2 : ℝ) * (↑x.2.1 : ℝ)) ⋯

Tactic:
fun_prop
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type ?u.110642
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
δ : α
s t : (↑unitInterval : Type)
ha : 0 ≤ (↑s : ℝ) * (1 - (↑t : ℝ))
hb : 0 ≤ 1 - (↑s : ℝ) * (↑t : ℝ)
⊢ 0 ≤ (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ))

Tactic:
apply div_nonneg

Premises used: div_nonneg
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type ?u.110642
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
δ : α
s t : (↑unitInterval : Type)
nlinarith : (↑s : ℝ) * (1 - (↑t : ℝ)) < 0 → (↑s : ℝ) * (1 - (↑t : ℝ)) - 0 + (0 - (0 - (↑s : ℝ)) * ((↑t : ℝ) - 1)) = 0
⊢ 0 ≤ (↑s : ℝ) * (1 - (↑t : ℝ))

Tactic:
nlinarith [s.2.1, t.2.2]

Premises used: And.right, And.left, Subtype.property
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type ?u.110642
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
δ : α
s t : (↑unitInterval : Type)
nlinarith :
  1 - (↑s : ℝ) * (↑t : ℝ) < 0 → 1 - (↑s : ℝ) * (↑t : ℝ) - 0 + ((↑t : ℝ) - 1) + (0 - ((↑s : ℝ) - 1) * (0 - (↑t : ℝ))) = 0
⊢ 0 ≤ 1 - (↑s : ℝ) * (↑t : ℝ)

Tactic:
nlinarith [s.2.2, t.2.2, t.2.1]

Premises used: And.right, And.left, Subtype.property
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type ?u.110642
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
δ : α
s t : (↑unitInterval : Type)
h₁ : (↑s : ℝ) * (1 - (↑t : ℝ)) ≤ 1 - (↑s : ℝ) * (↑t : ℝ)
hb : 0 ≤ 1 - (↑s : ℝ) * (↑t : ℝ)
⊢ (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ)) ≤ 1

Tactic:
apply div_le_one_of_le₀

Premises used: div_le_one_of_le₀
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type ?u.110642
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
δ : α
s t : (↑unitInterval : Type)
nlinarith :
  1 - (↑s : ℝ) * (↑t : ℝ) < (↑s : ℝ) * (1 - (↑t : ℝ)) →
    1 - (↑s : ℝ) * (↑t : ℝ) - (↑s : ℝ) * (1 - (↑t : ℝ)) + ((↑s : ℝ) - 1) = 0
⊢ (↑s : ℝ) * (1 - (↑t : ℝ)) ≤ 1 - (↑s : ℝ) * (↑t : ℝ)

Tactic:
nlinarith [s.2.2]

Premises used: And.right, Subtype.property
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
simp :
  (1 - (↑s : ℝ)) * (↑x : ℝ) + (↑s : ℝ) * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
    (1 - (↑s : ℝ) * (↑t : ℝ)) *
        ((1 - (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ))) * (↑x : ℝ) +
          (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ)) * (↑y : ℝ)) +
      (↑s : ℝ) * (↑t : ℝ) * (↑z : ℝ)
⊢ convexComb x (convexComb y z t) s =
    convexComb (convexComb x y (convexComb_assoc_coeff₁ s t)) z (convexComb_assoc_coeff₂ s t)

Tactic:
simp only [convexComb, coe_mul, Subtype.mk.injEq]

Premises used: Set.Icc.convexComb, Set.Icc.coe_mul, Subtype.mk.injEq
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
pos :
  ∀ (hs : (↑s : ℝ) = 1),
    (1 - (↑s : ℝ)) * (↑x : ℝ) + (↑s : ℝ) * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
      (1 - (↑s : ℝ) * (↑t : ℝ)) *
          ((1 - (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ))) * (↑x : ℝ) +
            (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ)) * (↑y : ℝ)) +
        (↑s : ℝ) * (↑t : ℝ) * (↑z : ℝ)
neg :
  ∀ (hs : ¬(↑s : ℝ) = 1),
    (1 - (↑s : ℝ)) * (↑x : ℝ) + (↑s : ℝ) * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
      (1 - (↑s : ℝ) * (↑t : ℝ)) *
          ((1 - (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ))) * (↑x : ℝ) +
            (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ)) * (↑y : ℝ)) +
        (↑s : ℝ) * (↑t : ℝ) * (↑z : ℝ)
⊢ (1 - (↑s : ℝ)) * (↑x : ℝ) + (↑s : ℝ) * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
    (1 - (↑s : ℝ) * (↑t : ℝ)) *
        ((1 - (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ))) * (↑x : ℝ) +
          (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ)) * (↑y : ℝ)) +
      (↑s : ℝ) * (↑t : ℝ) * (↑z : ℝ)

Tactic:
by_cases hs : (s : ℝ) = 1

Premises used: Subtype.val
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
hs : (↑s : ℝ) = 1
pos :
  HSub.hSub (α := ℝ) 1 1 * (↑x : ℝ) + 1 * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
    (1 - 1 * (↑t : ℝ)) *
        ((1 - 1 * (1 - (↑t : ℝ)) / (1 - 1 * (↑t : ℝ))) * (↑x : ℝ) +
          1 * (1 - (↑t : ℝ)) / (1 - 1 * (↑t : ℝ)) * (↑y : ℝ)) +
      1 * (↑t : ℝ) * (↑z : ℝ)
⊢ (1 - (↑s : ℝ)) * (↑x : ℝ) + (↑s : ℝ) * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
    (1 - (↑s : ℝ) * (↑t : ℝ)) *
        ((1 - (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ))) * (↑x : ℝ) +
          (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ)) * (↑y : ℝ)) +
      (↑s : ℝ) * (↑t : ℝ) * (↑z : ℝ)

Tactic:
simp only [hs]
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
hs : (↑s : ℝ) = 1
pos :
  ∀ (ht : (↑t : ℝ) = 1),
    HSub.hSub (α := ℝ) 1 1 * (↑x : ℝ) + 1 * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
      (1 - 1 * (↑t : ℝ)) *
          ((1 - 1 * (1 - (↑t : ℝ)) / (1 - 1 * (↑t : ℝ))) * (↑x : ℝ) +
            1 * (1 - (↑t : ℝ)) / (1 - 1 * (↑t : ℝ)) * (↑y : ℝ)) +
        1 * (↑t : ℝ) * (↑z : ℝ)
neg :
  ∀ (ht : ¬(↑t : ℝ) = 1),
    HSub.hSub (α := ℝ) 1 1 * (↑x : ℝ) + 1 * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
      (1 - 1 * (↑t : ℝ)) *
          ((1 - 1 * (1 - (↑t : ℝ)) / (1 - 1 * (↑t : ℝ))) * (↑x : ℝ) +
            1 * (1 - (↑t : ℝ)) / (1 - 1 * (↑t : ℝ)) * (↑y : ℝ)) +
        1 * (↑t : ℝ) * (↑z : ℝ)
⊢ HSub.hSub (α := ℝ) 1 1 * (↑x : ℝ) + 1 * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
    (1 - 1 * (↑t : ℝ)) *
        ((1 - 1 * (1 - (↑t : ℝ)) / (1 - 1 * (↑t : ℝ))) * (↑x : ℝ) +
          1 * (1 - (↑t : ℝ)) / (1 - 1 * (↑t : ℝ)) * (↑y : ℝ)) +
      1 * (↑t : ℝ) * (↑z : ℝ)

Tactic:
by_cases ht : (t : ℝ) = 1

Premises used: Subtype.val
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
hs : (↑s : ℝ) = 1
ht : (↑t : ℝ) = 1
⊢ HSub.hSub (α := ℝ) 1 1 * (↑x : ℝ) + 1 * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
    (1 - 1 * (↑t : ℝ)) *
        ((1 - 1 * (1 - (↑t : ℝ)) / (1 - 1 * (↑t : ℝ))) * (↑x : ℝ) +
          1 * (1 - (↑t : ℝ)) / (1 - 1 * (↑t : ℝ)) * (↑y : ℝ)) +
      1 * (↑t : ℝ) * (↑z : ℝ)

Tactic:
simp [ht]
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
hs : (↑s : ℝ) = 1
ht : ¬(↑t : ℝ) = 1
⊢ 1 - (↑t : ℝ) ≠ 0

Tactic:
grind
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
hs : (↑s : ℝ) = 1
ht : ¬(↑t : ℝ) = 1
⊢ 1 - (↑t : ℝ) ≠ 0

Tactic:
have : (1 - t : ℝ) ≠ 0 := by grind
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
hs : (↑s : ℝ) = 1
ht : ¬(↑t : ℝ) = 1
this : 1 - (↑t : ℝ) ≠ 0
neg :
  HSub.hSub (α := ℝ) 1 1 * (↑x : ℝ) + ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
    (1 - (↑t : ℝ)) * (HSub.hSub (α := ℝ) 1 1 * (↑x : ℝ) + (↑y : ℝ)) + (↑t : ℝ) * (↑z : ℝ)
⊢ HSub.hSub (α := ℝ) 1 1 * (↑x : ℝ) + 1 * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
    (1 - 1 * (↑t : ℝ)) *
        ((1 - 1 * (1 - (↑t : ℝ)) / (1 - 1 * (↑t : ℝ))) * (↑x : ℝ) +
          1 * (1 - (↑t : ℝ)) / (1 - 1 * (↑t : ℝ)) * (↑y : ℝ)) +
      1 * (↑t : ℝ) * (↑z : ℝ)

Tactic:
field_simp
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
hs : (↑s : ℝ) = 1
ht : ¬(↑t : ℝ) = 1
this : 1 - (↑t : ℝ) ≠ 0
⊢ HSub.hSub (α := ℝ) 1 1 * (↑x : ℝ) + ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
    (1 - (↑t : ℝ)) * (HSub.hSub (α := ℝ) 1 1 * (↑x : ℝ) + (↑y : ℝ)) + (↑t : ℝ) * (↑z : ℝ)

Tactic:
simp
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
hs : ¬(↑s : ℝ) = 1
pos :
  ∀ (ht : (↑t : ℝ) = 1),
    (1 - (↑s : ℝ)) * (↑x : ℝ) + (↑s : ℝ) * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
      (1 - (↑s : ℝ) * (↑t : ℝ)) *
          ((1 - (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ))) * (↑x : ℝ) +
            (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ)) * (↑y : ℝ)) +
        (↑s : ℝ) * (↑t : ℝ) * (↑z : ℝ)
neg :
  ∀ (ht : ¬(↑t : ℝ) = 1),
    (1 - (↑s : ℝ)) * (↑x : ℝ) + (↑s : ℝ) * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
      (1 - (↑s : ℝ) * (↑t : ℝ)) *
          ((1 - (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ))) * (↑x : ℝ) +
            (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ)) * (↑y : ℝ)) +
        (↑s : ℝ) * (↑t : ℝ) * (↑z : ℝ)
⊢ (1 - (↑s : ℝ)) * (↑x : ℝ) + (↑s : ℝ) * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
    (1 - (↑s : ℝ) * (↑t : ℝ)) *
        ((1 - (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ))) * (↑x : ℝ) +
          (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ)) * (↑y : ℝ)) +
      (↑s : ℝ) * (↑t : ℝ) * (↑z : ℝ)

Tactic:
by_cases ht : (t : ℝ) = 1

Premises used: Subtype.val
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
hs : ¬(↑s : ℝ) = 1
ht : (↑t : ℝ) = 1
⊢ (1 - (↑s : ℝ)) * (↑x : ℝ) + (↑s : ℝ) * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
    (1 - (↑s : ℝ) * (↑t : ℝ)) *
        ((1 - (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ))) * (↑x : ℝ) +
          (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ)) * (↑y : ℝ)) +
      (↑s : ℝ) * (↑t : ℝ) * (↑z : ℝ)

Tactic:
simp [ht]
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
hs : ¬(↑s : ℝ) = 1
ht : ¬(↑t : ℝ) = 1
h : 1 - (↑s : ℝ) * (↑t : ℝ) = 0
nlinarith : (↑t : ℝ) < 1 → 1 - (↑s : ℝ) * (↑t : ℝ) - 0 + ((↑t : ℝ) - 1) + (0 - ((↑s : ℝ) - 1) * (0 - (↑t : ℝ))) = 0
⊢ 1 ≤ (↑t : ℝ)

Tactic:
nlinarith [s.2.2, t.2.1]

Premises used: And.right, And.left, Subtype.property
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
hs : ¬(↑s : ℝ) = 1
ht : ¬(↑t : ℝ) = 1
h : 1 - (↑s : ℝ) * (↑t : ℝ) = 0
⊢ 1 ≤ (↑t : ℝ)

Tactic:
have : 1 ≤ (t : ℝ) := by nlinarith [s.2.2, t.2.1]
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
hs : ¬(↑s : ℝ) = 1
ht : ¬(↑t : ℝ) = 1
h : 1 - (↑s : ℝ) * (↑t : ℝ) = 0
this : 1 ≤ (↑t : ℝ)
⊢ False

Tactic:
grind
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
hs : ¬(↑s : ℝ) = 1
ht : ¬(↑t : ℝ) = 1
⊢ 1 - (↑s : ℝ) * (↑t : ℝ) ≠ 0

Tactic:
have : (1 - s * t : ℝ) ≠ 0 := by
        intro h
        have : 1 ≤ (t : ℝ) := by nlinarith [s.2.2, t.2.1]
        grind
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
hs : ¬(↑s : ℝ) = 1
ht : ¬(↑t : ℝ) = 1
this : 1 - (↑s : ℝ) * (↑t : ℝ) ≠ 0
neg :
  (1 - (↑s : ℝ)) * (↑x : ℝ) + (↑s : ℝ) * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
    (↑x : ℝ) * (1 - (↑s : ℝ) * (↑t : ℝ) - (↑s : ℝ) * (1 - (↑t : ℝ))) + (↑s : ℝ) * (1 - (↑t : ℝ)) * (↑y : ℝ) +
      (↑s : ℝ) * (↑t : ℝ) * (↑z : ℝ)
⊢ (1 - (↑s : ℝ)) * (↑x : ℝ) + (↑s : ℝ) * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
    (1 - (↑s : ℝ) * (↑t : ℝ)) *
        ((1 - (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ))) * (↑x : ℝ) +
          (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ)) * (↑y : ℝ)) +
      (↑s : ℝ) * (↑t : ℝ) * (↑z : ℝ)

Tactic:
field_simp
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
hs : ¬(↑s : ℝ) = 1
ht : ¬(↑t : ℝ) = 1
this : 1 - (↑s : ℝ) * (↑t : ℝ) ≠ 0
⊢ (1 - (↑s : ℝ)) * (↑x : ℝ) + (↑s : ℝ) * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
    (↑x : ℝ) * (1 - (↑s : ℝ) * (↑t : ℝ) - (↑s : ℝ) * (1 - (↑t : ℝ))) + (↑s : ℝ) * (1 - (↑t : ℝ)) * (↑y : ℝ) +
      (↑s : ℝ) * (↑t : ℝ) * (↑z : ℝ)

Tactic:
ring_nf
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
rw :
  convexComb x (convexComb z y (convexComb_assoc_coeff₁ (unitInterval.symm t) (unitInterval.symm s)))
      (unitInterval.symm (convexComb_assoc_coeff₂ (unitInterval.symm t) (unitInterval.symm s))) =
    convexComb x (convexComb z y (unitInterval.symm (convexComb_assoc_coeff₂' s t))) (convexComb_assoc_coeff₁' s t)
⊢ convexComb (convexComb x y s) z t =
    convexComb x (convexComb y z (convexComb_assoc_coeff₂' s t)) (convexComb_assoc_coeff₁' s t)

Tactic:
rw [← convexComb_symm, ← convexComb_symm y x, convexComb_assoc, ← convexComb_symm x,
    ← convexComb_symm z y]

Premises used: Set.Icc.convexComb_symm, Set.Icc.convexComb_assoc
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
rw :
  convexComb x (convexComb z y (convexComb_assoc_coeff₁ (unitInterval.symm t) (unitInterval.symm s)))
      (unitInterval.symm (convexComb_assoc_coeff₂ (unitInterval.symm t) (unitInterval.symm s))) =
    convexComb x (convexComb z y (unitInterval.symm (convexComb_assoc_coeff₂' s t)))
      (unitInterval.symm (convexComb_assoc_coeff₂ (unitInterval.symm t) (unitInterval.symm s)))
rw₁ :
  convexComb x (convexComb z y (convexComb_assoc_coeff₁ (unitInterval.symm t) (unitInterval.symm s)))
      (unitInterval.symm (convexComb_assoc_coeff₂ (unitInterval.symm t) (unitInterval.symm s))) =
    convexComb x
      (convexComb z y
        (unitInterval.symm (unitInterval.symm (convexComb_assoc_coeff₁ (unitInterval.symm t) (unitInterval.symm s)))))
      (unitInterval.symm (convexComb_assoc_coeff₂ (unitInterval.symm t) (unitInterval.symm s)))
rw₂ rw₃ :
  convexComb x (convexComb z y (convexComb_assoc_coeff₁ (unitInterval.symm t) (unitInterval.symm s)))
      (unitInterval.symm (convexComb_assoc_coeff₂ (unitInterval.symm t) (unitInterval.symm s))) =
    convexComb x (convexComb z y (convexComb_assoc_coeff₁ (unitInterval.symm t) (unitInterval.symm s)))
      (unitInterval.symm (convexComb_assoc_coeff₂ (unitInterval.symm t) (unitInterval.symm s)))
⊢ convexComb x (convexComb z y (convexComb_assoc_coeff₁ (unitInterval.symm t) (unitInterval.symm s)))
      (unitInterval.symm (convexComb_assoc_coeff₂ (unitInterval.symm t) (unitInterval.symm s))) =
    convexComb x (convexComb z y (unitInterval.symm (convexComb_assoc_coeff₂' s t))) (convexComb_assoc_coeff₁' s t)

Tactic:
rw [convexComb_assoc_coeff₁', convexComb_assoc_coeff₂', unitInterval.symm_symm]

Premises used: Set.Icc.convexComb_assoc_coeff₂', unitInterval.symm_symm, Set.Icc.convexComb_assoc_coeff₁'
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hxy : x ≤ y
hyz : y ≤ z
pos : ∀ (h : (↑z : ℝ) - (↑x : ℝ) = 0), 0 ≤ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))
neg : ∀ (h : ¬(↑z : ℝ) - (↑x : ℝ) = 0), 0 ≤ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))
⊢ 0 ≤ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))

Tactic:
by_cases h : (z - x : ℝ) = 0

Premises used: HSub.hSub, Subtype.val