awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
⊢ (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 : ℝ)
have 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 : ℝ)
Tactic: by_cases hs : (s : ℝ) = 1
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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 : ℝ)
⊢ (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 : ℝ)
have 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 : ℝ)
Tactic: by_cases hs : (s : ℝ) = 1
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
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 : ℝ)
have 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 : ℝ)
Tactic: simp only [hs]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
hs : (↑s : ℝ) = 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 : ℝ)
have 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 : ℝ)
Tactic: by_cases ht : (t : ℝ) = 1
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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 : ℝ)
⊢ 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 : ℝ)
have 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 : ℝ)
Tactic: by_cases ht : (t : ℝ) = 1
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (hypothesis)
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 : ℝ)
have this : 1 - (↑t : ℝ) ≠ 0
Tactic: have : (1 - t : ℝ) ≠ 0 := by grind
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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 * ((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 : ℝ)
have neg : HSub.hSub (α := ℝ) 1 1 * (↑x : ℝ) + ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
  (1 - (↑t : ℝ)) * (HSub.hSub (α := ℝ) 1 1 * (↑x : ℝ) + (↑y : ℝ)) + (↑t : ℝ) * (↑z : ℝ)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
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 : ℝ)
have 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 : ℝ)
Tactic: by_cases ht : (t : ℝ) = 1
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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 : ℝ)
⊢ (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 : ℝ)
have 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 : ℝ)
Tactic: by_cases ht : (t : ℝ) = 1
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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 : ℝ)
have nlinarith : (↑t : ℝ) < 1 → 1 - (↑s : ℝ) * (↑t : ℝ) - 0 + ((↑t : ℝ) - 1) + (0 - ((↑s : ℝ) - 1) * (0 - (↑t : ℝ))) = 0
Tactic: nlinarith [s.2.2, t.2.1]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (hypothesis)
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
⊢ False
have this : 1 ≤ (↑t : ℝ)
Tactic: have : 1 ≤ (t : ℝ) := by nlinarith [s.2.2, t.2.1]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (hypothesis)
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 : ℝ)
have this : 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
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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 : ℝ)) =
    (1 - (↑s : ℝ) * (↑t : ℝ)) *
        ((1 - (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ))) * (↑x : ℝ) +
          (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ)) * (↑y : ℝ)) +
      (↑s : ℝ) * (↑t : ℝ) * (↑z : ℝ)
have neg : (1 - (↑s : ℝ)) * (↑x : ℝ) + (↑s : ℝ) * ((1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑z : ℝ)) =
  (↑x : ℝ) * (1 - (↑s : ℝ) * (↑t : ℝ) - (↑s : ℝ) * (1 - (↑t : ℝ))) + (↑s : ℝ) * (1 - (↑t : ℝ)) * (↑y : ℝ) +
    (↑s : ℝ) * (↑t : ℝ) * (↑z : ℝ)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
⊢ convexComb (convexComb x y s) z t =
    convexComb x (convexComb y z (convexComb_assoc_coeff₂' s t)) (convexComb_assoc_coeff₁' s t)
have 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)
Tactic: rw [← convexComb_symm, ← convexComb_symm y x, convexComb_assoc, ← convexComb_symm x,
    ← convexComb_symm z y]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
s t : (↑unitInterval : Type)
⊢ 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)
have 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)))
Tactic: rw [convexComb_assoc_coeff₁', convexComb_assoc_coeff₂', unitInterval.symm_symm]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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)))
⊢ 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)
have 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)))
Tactic: rw [convexComb_assoc_coeff₁', convexComb_assoc_coeff₂', unitInterval.symm_symm]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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)))
⊢ 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)
have 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)))
Tactic: rw [convexComb_assoc_coeff₁', convexComb_assoc_coeff₂', unitInterval.symm_symm]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hxy : x ≤ y
hyz : y ≤ z
⊢ 0 ≤ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))
have pos : ∀ (h : (↑z : ℝ) - (↑x : ℝ) = 0), 0 ≤ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))
Tactic: by_cases h : (z - x : ℝ) = 0
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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 : ℝ))
⊢ 0 ≤ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))
have neg : ∀ (h : ¬(↑z : ℝ) - (↑x : ℝ) = 0), 0 ≤ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))
Tactic: by_cases h : (z - x : ℝ) = 0
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (hypothesis)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hxy : x ≤ y
hyz : y ≤ z
h : ¬(↑z : ℝ) - (↑x : ℝ) = 0
⊢ 0 ≤ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))
have hxy₁ : (↑x : ℝ) ≤ (↑y : ℝ)
Tactic: replace hxy : (x : ℝ) ≤ (y : ℝ) := hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (hypothesis)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hyz : y ≤ z
h : ¬(↑z : ℝ) - (↑x : ℝ) = 0
hxy : (↑x : ℝ) ≤ (↑y : ℝ)
⊢ 0 ≤ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))
have hyz₁ : (↑y : ℝ) ≤ (↑z : ℝ)
Tactic: replace hyz : (y : ℝ) ≤ (z : ℝ) := hyz
Cleared hypotheses: hyz
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
h : ¬(↑z : ℝ) - (↑x : ℝ) = 0
hxy : (↑x : ℝ) ≤ (↑y : ℝ)
hyz : (↑y : ℝ) ≤ (↑z : ℝ)
⊢ 0 ≤ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))
have neg : 0 ≤ (↑y : ℝ) - (↑x : ℝ)
Tactic: apply div_nonneg
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
h : ¬(↑z : ℝ) - (↑x : ℝ) = 0
hxy : (↑x : ℝ) ≤ (↑y : ℝ)
hyz : (↑y : ℝ) ≤ (↑z : ℝ)
neg : 0 ≤ (↑y : ℝ) - (↑x : ℝ)
⊢ 0 ≤ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))
have neg₁ : 0 ≤ (↑z : ℝ) - (↑x : ℝ)
Tactic: apply div_nonneg
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hxy : x ≤ y
hyz : y ≤ z
⊢ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) ≤ 1
have pos : ∀ (h : (↑z : ℝ) - (↑x : ℝ) = 0), ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) ≤ 1
Tactic: by_cases h : (z - x : ℝ) = 0
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hxy : x ≤ y
hyz : y ≤ z
pos : ∀ (h : (↑z : ℝ) - (↑x : ℝ) = 0), ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) ≤ 1
⊢ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) ≤ 1
have neg : ∀ (h : ¬(↑z : ℝ) - (↑x : ℝ) = 0), ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) ≤ 1
Tactic: by_cases h : (z - x : ℝ) = 0
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (hypothesis)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hxy : x ≤ y
hyz : y ≤ z
h : ¬(↑z : ℝ) - (↑x : ℝ) = 0
⊢ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) ≤ 1
have hxy₁ : (↑x : ℝ) ≤ (↑y : ℝ)
Tactic: replace hxy : (x : ℝ) ≤ (y : ℝ) := hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (hypothesis)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hyz : y ≤ z
h : ¬(↑z : ℝ) - (↑x : ℝ) = 0
hxy : (↑x : ℝ) ≤ (↑y : ℝ)
⊢ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) ≤ 1
have hyz₁ : (↑y : ℝ) ≤ (↑z : ℝ)
Tactic: replace hyz : (y : ℝ) ≤ (z : ℝ) := hyz
Cleared hypotheses: hyz
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
h : ¬(↑z : ℝ) - (↑x : ℝ) = 0
hxy : (↑x : ℝ) ≤ (↑y : ℝ)
hyz : (↑y : ℝ) ≤ (↑z : ℝ)
⊢ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) ≤ 1
have neg : (↑y : ℝ) - (↑x : ℝ) ≤ (↑z : ℝ) - (↑x : ℝ)
Tactic: apply div_le_one_of_le₀
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
h : ¬(↑z : ℝ) - (↑x : ℝ) = 0
hxy : (↑x : ℝ) ≤ (↑y : ℝ)
hyz : (↑y : ℝ) ≤ (↑z : ℝ)
neg : (↑y : ℝ) - (↑x : ℝ) ≤ (↑z : ℝ) - (↑x : ℝ)
⊢ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) ≤ 1
have neg₁ : 0 ≤ (↑z : ℝ) - (↑x : ℝ)
Tactic: apply div_le_one_of_le₀
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hxy : x ≤ y
hyz : y ≤ z
⊢ y =
    convexComb x z (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) (((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))) ⋯)
have a₁ : (↑y : ℝ) =
  (↑(convexComb x z
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) (((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))) sorry)) :
    ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hxy : x ≤ y
hyz : y ≤ z
⊢ (↑y : ℝ) =
    (1 - ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))) * (↑x : ℝ) +
      ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) * (↑z : ℝ)
have pos : ∀ (h : (↑z : ℝ) - (↑x : ℝ) = 0),
  (↑y : ℝ) =
    (1 - ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))) * (↑x : ℝ) +
      ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) * (↑z : ℝ)
Tactic: by_cases h : (z - x : ℝ) = 0
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hxy : x ≤ y
hyz : y ≤ z
pos :
  ∀ (h : (↑z : ℝ) - (↑x : ℝ) = 0),
    (↑y : ℝ) =
      (1 - ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))) * (↑x : ℝ) +
        ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) * (↑z : ℝ)
⊢ (↑y : ℝ) =
    (1 - ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))) * (↑x : ℝ) +
      ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) * (↑z : ℝ)
have neg : ∀ (h : ¬(↑z : ℝ) - (↑x : ℝ) = 0),
  (↑y : ℝ) =
    (1 - ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))) * (↑x : ℝ) +
      ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) * (↑z : ℝ)
Tactic: by_cases h : (z - x : ℝ) = 0
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hxy : x ≤ y
hyz : y ≤ z
h : (↑z : ℝ) - (↑x : ℝ) = 0
⊢ (↑y : ℝ) =
    (1 - ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))) * (↑x : ℝ) +
      ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) * (↑z : ℝ)
have pos : (↑y : ℝ) = (↑x : ℝ)
Tactic: simp_all only [div_zero, sub_zero, one_mul, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (hypothesis)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hxy : x ≤ y
hyz : y ≤ z
h : (↑z : ℝ) - (↑x : ℝ) = 0
⊢ (↑y : ℝ) = (↑x : ℝ)
have hxy₁ : (↑x : ℝ) ≤ (↑y : ℝ)
Tactic: replace hxy : (x : ℝ) ≤ (y : ℝ) := hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (hypothesis)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hyz : y ≤ z
h : (↑z : ℝ) - (↑x : ℝ) = 0
hxy : (↑x : ℝ) ≤ (↑y : ℝ)
⊢ (↑y : ℝ) = (↑x : ℝ)
have hyz₁ : (↑y : ℝ) ≤ (↑z : ℝ)
Tactic: replace hyz : (y : ℝ) ≤ (z : ℝ) := hyz
Cleared hypotheses: hyz
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
h : (↑z : ℝ) - (↑x : ℝ) = 0
hxy : (↑x : ℝ) ≤ (↑y : ℝ)
hyz : (↑y : ℝ) ≤ (↑z : ℝ)
⊢ (↑y : ℝ) = (↑x : ℝ)
have linarith : (↑y : ℝ) < (↑x : ℝ) → (↑x : ℝ) - (↑y : ℝ) + ((↑y : ℝ) - (↑x : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
h : (↑z : ℝ) - (↑x : ℝ) = 0
hxy : (↑x : ℝ) ≤ (↑y : ℝ)
hyz : (↑y : ℝ) ≤ (↑z : ℝ)
linarith : (↑y : ℝ) < (↑x : ℝ) → (↑x : ℝ) - (↑y : ℝ) + ((↑y : ℝ) - (↑x : ℝ)) = 0
⊢ (↑y : ℝ) = (↑x : ℝ)
have linarith₁ : (↑x : ℝ) < (↑y : ℝ) → (↑z : ℝ) - (↑x : ℝ) - 0 + ((↑y : ℝ) - (↑z : ℝ)) + ((↑x : ℝ) - (↑y : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hxy : x ≤ y
hyz : y ≤ z
h : ¬(↑z : ℝ) - (↑x : ℝ) = 0
⊢ (↑y : ℝ) =
    (1 - ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))) * (↑x : ℝ) +
      ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) * (↑z : ℝ)
have neg : (↑y : ℝ) * ((↑z : ℝ) - (↑x : ℝ)) =
  (↑x : ℝ) * ((↑z : ℝ) - (↑x : ℝ) - ((↑y : ℝ) - (↑x : ℝ))) + ((↑y : ℝ) - (↑x : ℝ)) * (↑z : ℝ)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
ι : Sort u_1
a b : ℝ
h : a ≤ b
c : ι → Set (↑(Icc a b) : Type)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set (↑(Icc a b) : Type)) univ (⋃ (i : ι), c i)
⊢ ∃ (t : ℕ → (↑(Icc a b) : Type)),
    (↑(t 0) : ℝ) = a ∧
      Monotone t ∧ (∃ (m : ℕ), ∀ n ≥ m, (↑(t n) : ℝ) = b) ∧ ∀ (n : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ⊆ c i
have obtain : ∀ (δ : ℝ) (δ_pos : δ > 0)
  (ball_subset :
    ∀ (x : (↑(Icc a b) : Type)),
      Membership.mem (γ := Set (↑(Icc a b) : Type)) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i),
  ∃ (t : ℕ → (↑(Icc a b) : Type)),
    (↑(t 0) : ℝ) = a ∧
      Monotone t ∧ (∃ (m : ℕ), ∀ n ≥ m, (↑(t n) : ℝ) = b) ∧ ∀ (n : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ⊆ c i
Tactic: obtain ⟨δ, δ_pos, ball_subset⟩ := lebesgue_number_lemma_of_metric isCompact_univ hc₁ hc₂
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (hypothesis)
Goal:
ι : Sort u_1
a b : ℝ
h : a ≤ b
c : ι → Set (↑(Icc a b) : Type)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set (↑(Icc a b) : Type)) univ (⋃ (i : ι), c i)
δ : ℝ
δ_pos : δ > 0
ball_subset :
  ∀ (x : (↑(Icc a b) : Type)), Membership.mem (γ := Set (↑(Icc a b) : Type)) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i
⊢ ∃ (t : ℕ → (↑(Icc a b) : Type)),
    (↑(t 0) : ℝ) = a ∧
      Monotone t ∧ (∃ (m : ℕ), ∀ n ≥ m, (↑(t n) : ℝ) = b) ∧ ∀ (n : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ⊆ c i
have hδ : 0 < δ / 2
Tactic: have hδ := half_pos δ_pos