awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UnitInterval
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 : ℝ))

Tactic:
simp_all
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hxy : x ≤ y
hyz : y ≤ z
h : ¬(↑z : ℝ) - (↑x : ℝ) = 0
⊢ (↑x : ℝ) ≤ (↑y : ℝ)

Tactic:
replace hxy : (x : ℝ) ≤ (y : ℝ) := hxy
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hyz : y ≤ z
h : ¬(↑z : ℝ) - (↑x : ℝ) = 0
hxy : (↑x : ℝ) ≤ (↑y : ℝ)
⊢ (↑y : ℝ) ≤ (↑z : ℝ)

Tactic:
replace hyz : (y : ℝ) ≤ (z : ℝ) := hyz
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
h : ¬(↑z : ℝ) - (↑x : ℝ) = 0
hxy : (↑x : ℝ) ≤ (↑y : ℝ)
hyz : (↑y : ℝ) ≤ (↑z : ℝ)
neg : 0 ≤ (↑y : ℝ) - (↑x : ℝ)
neg₁ : 0 ≤ (↑z : ℝ) - (↑x : ℝ)
⊢ 0 ≤ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))

Tactic:
apply div_nonneg

Premises used: div_nonneg
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
h : ¬(↑z : ℝ) - (↑x : ℝ) = 0
hxy : (↑x : ℝ) ≤ (↑y : ℝ)
hyz : (↑y : ℝ) ≤ (↑z : ℝ)
⊢ 0 ≤ (↑y : ℝ) - (↑x : ℝ)

Tactic:
grind
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
h : ¬(↑z : ℝ) - (↑x : ℝ) = 0
hxy : (↑x : ℝ) ≤ (↑y : ℝ)
hyz : (↑y : ℝ) ≤ (↑z : ℝ)
⊢ 0 ≤ (↑z : ℝ) - (↑x : ℝ)

Tactic:
grind
-- 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), ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) ≤ 1
neg : ∀ (h : ¬(↑z : ℝ) - (↑x : ℝ) = 0), ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) ≤ 1
⊢ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) ≤ 1

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

Premises used: HSub.hSub, Subtype.val
-- Module: Mathlib.Topology.UnitInterval
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

Tactic:
simp_all
-- Module: Mathlib.Topology.UnitInterval
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 : ℝ)
neg₁ : 0 ≤ (↑z : ℝ) - (↑x : ℝ)
⊢ ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) ≤ 1

Tactic:
apply div_le_one_of_le₀

Premises used: div_le_one_of_le₀
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
h : ¬(↑z : ℝ) - (↑x : ℝ) = 0
hxy : (↑x : ℝ) ≤ (↑y : ℝ)
hyz : (↑y : ℝ) ≤ (↑z : ℝ)
⊢ (↑y : ℝ) - (↑x : ℝ) ≤ (↑z : ℝ) - (↑x : ℝ)

Tactic:
grind
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hxy : x ≤ y
hyz : y ≤ z
a₁ :
  (↑y : ℝ) =
    (↑(convexComb x z
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) (((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))) ⋯)) :
      ℝ)
⊢ y =
    convexComb x z (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) (((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))) ⋯)

Tactic:
ext
-- 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),
    (↑y : ℝ) =
      (1 - ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))) * (↑x : ℝ) +
        ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) * (↑z : ℝ)
neg :
  ∀ (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 : ℝ)

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

Premises used: HSub.hSub, Subtype.val
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hxy : x ≤ y
hyz : y ≤ z
h : (↑z : ℝ) - (↑x : ℝ) = 0
pos : (↑y : ℝ) = (↑x : ℝ)
⊢ (↑y : ℝ) =
    (1 - ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))) * (↑x : ℝ) +
      ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) * (↑z : ℝ)

Tactic:
simp_all only [div_zero, sub_zero, one_mul, zero_mul, add_zero]

Premises used: sub_zero, MulZeroClass.zero_mul, add_zero, div_zero, one_mul
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hxy : x ≤ y
hyz : y ≤ z
h : (↑z : ℝ) - (↑x : ℝ) = 0
⊢ (↑x : ℝ) ≤ (↑y : ℝ)

Tactic:
replace hxy : (x : ℝ) ≤ (y : ℝ) := hxy
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hyz : y ≤ z
h : (↑z : ℝ) - (↑x : ℝ) = 0
hxy : (↑x : ℝ) ≤ (↑y : ℝ)
⊢ (↑y : ℝ) ≤ (↑z : ℝ)

Tactic:
replace hyz : (y : ℝ) ≤ (z : ℝ) := hyz
-- Module: Mathlib.Topology.UnitInterval
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
linarith₁ : (↑x : ℝ) < (↑y : ℝ) → (↑z : ℝ) - (↑x : ℝ) - 0 + ((↑y : ℝ) - (↑z : ℝ)) + ((↑x : ℝ) - (↑y : ℝ)) = 0
⊢ (↑y : ℝ) = (↑x : ℝ)

Tactic:
linarith
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hxy : x ≤ y
hyz : y ≤ z
h : ¬(↑z : ℝ) - (↑x : ℝ) = 0
neg :
  (↑y : ℝ) * ((↑z : ℝ) - (↑x : ℝ)) =
    (↑x : ℝ) * ((↑z : ℝ) - (↑x : ℝ) - ((↑y : ℝ) - (↑x : ℝ))) + ((↑y : ℝ) - (↑x : ℝ)) * (↑z : ℝ)
⊢ (↑y : ℝ) =
    (1 - ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ))) * (↑x : ℝ) +
      ((↑y : ℝ) - (↑x : ℝ)) / ((↑z : ℝ) - (↑x : ℝ)) * (↑z : ℝ)

Tactic:
field_simp
-- Module: Mathlib.Topology.UnitInterval
Goal:
a b : ℝ
x y z : (↑(Icc a b) : Type)
hxy : x ≤ y
hyz : y ≤ z
h : ¬(↑z : ℝ) - (↑x : ℝ) = 0
⊢ (↑y : ℝ) * ((↑z : ℝ) - (↑x : ℝ)) =
    (↑x : ℝ) * ((↑z : ℝ) - (↑x : ℝ) - ((↑y : ℝ) - (↑x : ℝ))) + ((↑y : ℝ) - (↑x : ℝ)) * (↑z : ℝ)

Tactic:
ring_nf
-- Module: Mathlib.Topology.UnitInterval
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)
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
⊢ ∃ (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₂

Premises used: lebesgue_number_lemma_of_metric, isCompact_univ
-- Module: Mathlib.Topology.UnitInterval
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
⊢ 0 < δ / 2

Tactic:
have hδ := half_pos δ_pos
-- Module: Mathlib.Topology.UnitInterval
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
hδ : 0 < δ / 2
⊢ ∃ (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:
⟨addNSMul h (δ/2), addNSMul_zero h,
    monotone_addNSMul h hδ.le, addNSMul_eq_right h hδ, fun n ↦ ?_⟩

Premises used: Set.Icc.addNSMul_eq_right, Set.Icc.addNSMul_zero, HDiv.hDiv, LT.lt.le, Set.Icc.addNSMul, And.intro, Exists.intro, Set.Icc.monotone_addNSMul, OfNat.ofNat
-- Module: Mathlib.Topology.UnitInterval
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
hδ : 0 < δ / 2
refine : ∀ (n : ℕ), ∃ (i : ι), Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ⊆ 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:
refine ⟨addNSMul h (δ/2), addNSMul_zero h,
    monotone_addNSMul h hδ.le, addNSMul_eq_right h hδ, fun n ↦ ?_⟩
-- Module: Mathlib.Topology.UnitInterval
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
hδ : 0 < δ / 2
n : ℕ
obtain :
  ∀ (i : ι) (hsub : Metric.ball (addNSMul h (δ / 2) n) δ ⊆ c i),
    ∃ (i : ι), Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ⊆ c i
⊢ ∃ (i : ι), Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ⊆ c i

Tactic:
obtain ⟨i, hsub⟩ := ball_subset (addNSMul h (δ / 2) n) trivial

Premises used: trivial, HDiv.hDiv, Set.Icc.addNSMul, OfNat.ofNat
-- Module: Mathlib.Topology.UnitInterval
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
hδ : 0 < δ / 2
n : ℕ
i : ι
hsub : Metric.ball (addNSMul h (δ / 2) n) δ ⊆ c i
⊢ ∃ (i : ι), Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ⊆ c i

Tactic:
⟨i, fun t ht ↦ hsub ((abs_sub_addNSMul_le h hδ.le n ht).trans_lt <| half_lt_self δ_pos)⟩

Premises used: half_lt_self, LT.lt.le, Set.Icc.abs_sub_addNSMul_le, Exists.intro, LE.le.trans_lt
-- Module: Mathlib.Topology.UnitInterval
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
hδ : 0 < δ / 2
n : ℕ
i : ι
hsub : Metric.ball (addNSMul h (δ / 2) n) δ ⊆ c i
⊢ ∃ (i : ι), Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ⊆ c i

Tactic:
exact ⟨i, fun t ht ↦ hsub ((abs_sub_addNSMul_le h hδ.le n ht).trans_lt <| half_lt_self δ_pos)⟩
-- Module: Mathlib.Topology.UnitInterval
Goal:
ι : Sort u_1
c : ι → Set (↑I : Type)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set (↑I : Type)) univ (⋃ (i : ι), c i)
simp_rw :
  ∃ (t : ℕ → (↑I : Type)),
    (↑(t 0) : ℝ) = (↑0 : ℝ) ∧
      Monotone t ∧ (∃ (n : ℕ), ∀ m ≥ n, (↑(t m) : ℝ) = (↑1 : ℝ)) ∧ ∀ (n : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ⊆ c i
⊢ ∃ (t : ℕ → (↑I : Type)),
    t 0 = 0 ∧ Monotone t ∧ (∃ (n : ℕ), ∀ m ≥ n, t m = 1) ∧ ∀ (n : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ⊆ c i

Tactic:
simp_rw [← Subtype.coe_inj]

Premises used: Subtype.coe_inj
-- Module: Mathlib.Topology.UnitInterval
Goal:
ι : Sort u_1
c : ι → Set (↑I : Type)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set (↑I : Type)) univ (⋃ (i : ι), c i)
⊢ ∃ (t : ℕ → (↑I : Type)),
    (↑(t 0) : ℝ) = (↑0 : ℝ) ∧
      Monotone t ∧ (∃ (n : ℕ), ∀ m ≥ n, (↑(t m) : ℝ) = (↑1 : ℝ)) ∧ ∀ (n : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ⊆ c i

Tactic:
exists_monotone_Icc_subset_open_cover_Icc zero_le_one hc₁ hc₂

Premises used: exists_monotone_Icc_subset_open_cover_Icc, Set.Mem, zero_le_one
-- Module: Mathlib.Topology.UnitInterval
Goal:
ι : Sort u_1
c : ι → Set (↑I : Type)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set (↑I : Type)) univ (⋃ (i : ι), c i)
⊢ ∃ (t : ℕ → (↑I : Type)),
    (↑(t 0) : ℝ) = (↑0 : ℝ) ∧
      Monotone t ∧ (∃ (n : ℕ), ∀ m ≥ n, (↑(t m) : ℝ) = (↑1 : ℝ)) ∧ ∀ (n : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ⊆ c i

Tactic:
exact exists_monotone_Icc_subset_open_cover_Icc zero_le_one hc₁ hc₂

Premises used: exists_monotone_Icc_subset_open_cover_Icc, zero_le_one
-- Module: Mathlib.Topology.UnitInterval
Goal:
ι : Sort u_1
c : ι → Set ((↑I : Type) × (↑I : Type))
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set ((↑I : Type) × (↑I : Type))) univ (⋃ (i : ι), c i)
obtain :
  ∀ (δ : ℝ) (δ_pos : δ > 0)
    (ball_subset :
      ∀ (x : (↑I : Type) × (↑I : Type)),
        Membership.mem (γ := Set ((↑I : Type) × (↑I : Type))) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i),
    ∃ (t : ℕ → (↑I : Type)),
      t 0 = 0 ∧
        Monotone t ∧
          (∃ (n : ℕ), ∀ m ≥ n, t m = 1) ∧ ∀ (n m : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i
⊢ ∃ (t : ℕ → (↑I : Type)),
    t 0 = 0 ∧
      Monotone t ∧
        (∃ (n : ℕ), ∀ m ≥ n, t m = 1) ∧ ∀ (n m : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i

Tactic:
obtain ⟨δ, δ_pos, ball_subset⟩ := lebesgue_number_lemma_of_metric isCompact_univ hc₁ hc₂

Premises used: lebesgue_number_lemma_of_metric, isCompact_univ
-- Module: Mathlib.Topology.UnitInterval
Goal:
ι : Sort u_1
c : ι → Set ((↑I : Type) × (↑I : Type))
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set ((↑I : Type) × (↑I : Type))) univ (⋃ (i : ι), c i)
δ : ℝ
δ_pos : δ > 0
ball_subset :
  ∀ (x : (↑I : Type) × (↑I : Type)),
    Membership.mem (γ := Set ((↑I : Type) × (↑I : Type))) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i
⊢ 0 < δ / 2

Tactic:
have hδ := half_pos δ_pos
-- Module: Mathlib.Topology.UnitInterval
Goal:
ι : Sort u_1
c : ι → Set ((↑I : Type) × (↑I : Type))
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set ((↑I : Type) × (↑I : Type))) univ (⋃ (i : ι), c i)
δ : ℝ
δ_pos : δ > 0
ball_subset :
  ∀ (x : (↑I : Type) × (↑I : Type)),
    Membership.mem (γ := Set ((↑I : Type) × (↑I : Type))) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
simp_rw :
  ∃ (t : ℕ → (↑I : Type)),
    (↑(t 0) : ℝ) = (↑0 : ℝ) ∧
      Monotone t ∧
        (∃ (n : ℕ), ∀ m ≥ n, (↑(t m) : ℝ) = (↑1 : ℝ)) ∧
          ∀ (n m : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i
⊢ ∃ (t : ℕ → (↑I : Type)),
    t 0 = 0 ∧
      Monotone t ∧
        (∃ (n : ℕ), ∀ m ≥ n, t m = 1) ∧ ∀ (n m : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i

Tactic:
simp_rw [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Topology.UnitInterval
Goal:
ι : Sort u_1
c : ι → Set ((↑I : Type) × (↑I : Type))
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set ((↑I : Type) × (↑I : Type))) univ (⋃ (i : ι), c i)
δ : ℝ
δ_pos : δ > 0
ball_subset :
  ∀ (x : (↑I : Type) × (↑I : Type)),
    Membership.mem (γ := Set ((↑I : Type) × (↑I : Type))) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
⊢ LE.le (α := ℝ) 0 1

Tactic:
have h : (0 : ℝ) ≤ 1 := zero_le_one
-- Module: Mathlib.Topology.UnitInterval
Goal:
ι : Sort u_1
c : ι → Set ((↑I : Type) × (↑I : Type))
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set ((↑I : Type) × (↑I : Type))) univ (⋃ (i : ι), c i)
δ : ℝ
δ_pos : δ > 0
ball_subset :
  ∀ (x : (↑I : Type) × (↑I : Type)),
    Membership.mem (γ := Set ((↑I : Type) × (↑I : Type))) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
h : LE.le (α := ℝ) 0 1
⊢ ∃ (t : ℕ → (↑I : Type)),
    (↑(t 0) : ℝ) = (↑0 : ℝ) ∧
      Monotone t ∧
        (∃ (n : ℕ), ∀ m ≥ n, (↑(t m) : ℝ) = (↑1 : ℝ)) ∧
          ∀ (n m : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i

Tactic:
⟨addNSMul h (δ/2), addNSMul_zero h,
    monotone_addNSMul h hδ.le, addNSMul_eq_right h hδ, fun n m ↦ ?_⟩

Premises used: Set.Icc.addNSMul_eq_right, Set.Icc.addNSMul_zero, HDiv.hDiv, LT.lt.le, Set.Icc.addNSMul, And.intro, Exists.intro, Set.Icc.monotone_addNSMul, OfNat.ofNat
-- Module: Mathlib.Topology.UnitInterval
Goal:
ι : Sort u_1
c : ι → Set ((↑I : Type) × (↑I : Type))
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set ((↑I : Type) × (↑I : Type))) univ (⋃ (i : ι), c i)
δ : ℝ
δ_pos : δ > 0
ball_subset :
  ∀ (x : (↑I : Type) × (↑I : Type)),
    Membership.mem (γ := Set ((↑I : Type) × (↑I : Type))) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
h : LE.le (α := ℝ) 0 1
refine :
  ∀ (n m : ℕ),
    ∃ (i : ι),
      Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ×ˢ
          Icc (addNSMul h (δ / 2) m) (addNSMul h (δ / 2) (m + 1)) ⊆
        c i
⊢ ∃ (t : ℕ → (↑I : Type)),
    (↑(t 0) : ℝ) = (↑0 : ℝ) ∧
      Monotone t ∧
        (∃ (n : ℕ), ∀ m ≥ n, (↑(t m) : ℝ) = (↑1 : ℝ)) ∧
          ∀ (n m : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i

Tactic:
refine ⟨addNSMul h (δ/2), addNSMul_zero h,
    monotone_addNSMul h hδ.le, addNSMul_eq_right h hδ, fun n m ↦ ?_⟩
-- Module: Mathlib.Topology.UnitInterval
Goal:
ι : Sort u_1
c : ι → Set ((↑I : Type) × (↑I : Type))
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set ((↑I : Type) × (↑I : Type))) univ (⋃ (i : ι), c i)
δ : ℝ
δ_pos : δ > 0
ball_subset :
  ∀ (x : (↑I : Type) × (↑I : Type)),
    Membership.mem (γ := Set ((↑I : Type) × (↑I : Type))) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
h : LE.le (α := ℝ) 0 1
n m : ℕ
obtain :
  ∀ (i : ι) (hsub : Metric.ball (addNSMul h (δ / 2) n, addNSMul h (δ / 2) m) δ ⊆ c i),
    ∃ (i : ι),
      Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ×ˢ
          Icc (addNSMul h (δ / 2) m) (addNSMul h (δ / 2) (m + 1)) ⊆
        c i
⊢ ∃ (i : ι),
    Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ×ˢ Icc (addNSMul h (δ / 2) m) (addNSMul h (δ / 2) (m + 1)) ⊆
      c i

Tactic:
obtain ⟨i, hsub⟩ := ball_subset (addNSMul h (δ / 2) n, addNSMul h (δ / 2) m) trivial

Premises used: trivial, HDiv.hDiv, Prod.mk, Set.Icc.addNSMul, OfNat.ofNat
-- Module: Mathlib.Topology.UnitInterval
Goal:
ι : Sort u_1
c : ι → Set ((↑I : Type) × (↑I : Type))
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set ((↑I : Type) × (↑I : Type))) univ (⋃ (i : ι), c i)
δ : ℝ
δ_pos : δ > 0
ball_subset :
  ∀ (x : (↑I : Type) × (↑I : Type)),
    Membership.mem (γ := Set ((↑I : Type) × (↑I : Type))) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
h : LE.le (α := ℝ) 0 1
n m : ℕ
i : ι
hsub : Metric.ball (addNSMul h (δ / 2) n, addNSMul h (δ / 2) m) δ ⊆ c i
⊢ ∃ (i : ι),
    Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ×ˢ Icc (addNSMul h (δ / 2) m) (addNSMul h (δ / 2) (m + 1)) ⊆
      c i

Tactic:
⟨i, fun t ht ↦ hsub (Metric.mem_ball.mpr <| (max_le (abs_sub_addNSMul_le h hδ.le n ht.1) <|
    abs_sub_addNSMul_le h hδ.le m ht.2).trans_lt <| half_lt_self δ_pos)⟩

Premises used: half_lt_self, Iff.mpr, LT.lt.le, Metric.mem_ball, And.right, Set.Icc.abs_sub_addNSMul_le, And.left, max_le, Exists.intro, LE.le.trans_lt
-- Module: Mathlib.Topology.UnitInterval
Goal:
ι : Sort u_1
c : ι → Set ((↑I : Type) × (↑I : Type))
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set ((↑I : Type) × (↑I : Type))) univ (⋃ (i : ι), c i)
δ : ℝ
δ_pos : δ > 0
ball_subset :
  ∀ (x : (↑I : Type) × (↑I : Type)),
    Membership.mem (γ := Set ((↑I : Type) × (↑I : Type))) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
h : LE.le (α := ℝ) 0 1
n m : ℕ
i : ι
hsub : Metric.ball (addNSMul h (δ / 2) n, addNSMul h (δ / 2) m) δ ⊆ c i
⊢ ∃ (i : ι),
    Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ×ˢ Icc (addNSMul h (δ / 2) m) (addNSMul h (δ / 2) (m + 1)) ⊆
      c i

Tactic:
exact ⟨i, fun t ht ↦ hsub (Metric.mem_ball.mpr <| (max_le (abs_sub_addNSMul_le h hδ.le n ht.1) <|
    abs_sub_addNSMul_le h hδ.le m ht.2).trans_lt <| half_lt_self δ_pos)⟩
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : ℝ
⊢ Eq (α := (↑(Icc 0 1) : Type)) (projIcc 0 1 ⋯ x) 0 ↔ x ≤ 0

Tactic:
projIcc_eq_left zero_lt_one

Premises used: Set.Mem, Set.projIcc_eq_left, zero_lt_one
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : ℝ
⊢ Eq (α := (↑(Icc 0 1) : Type)) (projIcc 0 1 ⋯ x) 1 ↔ 1 ≤ x

Tactic:
projIcc_eq_right zero_lt_one

Premises used: Set.Mem, Set.projIcc_eq_right, zero_lt_one
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑unitInterval : Type)
⊢ 0 ≤ (↑x : ℝ)

Tactic:
unit_interval
-- Module: Mathlib.Topology.UnitInterval
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : IsTopologicalRing 𝕜
a b : 𝕜
h : 0 < a
⊢ image (α := 𝕜) (⇑(affineHomeomorph a b ⋯) : (a : 𝕜) → 𝕜) (Icc 0 1) = Icc b (a + b)

Tactic:
simp [h]
-- Module: Mathlib.Topology.UnitInterval
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : IsTopologicalRing 𝕜
a b : 𝕜
h : a < b
e : (↑(Icc 0 1) : Type u_1) ≃ₜ
  (↑(image (α := 𝕜) (⇑(affineHomeomorph (b - a) a ⋯) : (a : 𝕜) → 𝕜) (Icc 0 1)) : Type u_1) :=
  Homeomorph.image (affineHomeomorph (b - a) a ⋯) (Icc 0 1)
refine :
  (↑(image (α := 𝕜) (⇑(affineHomeomorph (b - a) a ⋯) : (a : 𝕜) → 𝕜) (Icc 0 1)) : Type u_1) ≃ₜ (↑(Icc a b) : Type u_1)
⊢ (↑(Icc a b) : Type u_1) ≃ₜ (↑(Icc 0 1) : Type u_1)

Tactic:
refine (e.trans ?_).symm

Premises used: Homeomorph.symm, Homeomorph.trans
-- Module: Mathlib.Topology.UnitInterval
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : IsTopologicalRing 𝕜
a b : 𝕜
h : a < b
e : (↑(Icc 0 1) : Type u_1) ≃ₜ
  (↑(image (α := 𝕜) (⇑(affineHomeomorph (b - a) a ⋯) : (a : 𝕜) → 𝕜) (Icc 0 1)) : Type u_1) :=
  Homeomorph.image (affineHomeomorph (b - a) a ⋯) (Icc 0 1)
h₁ : image (α := 𝕜) (⇑(affineHomeomorph (b - a) a ⋯) : (a : 𝕜) → 𝕜) (Icc 0 1) = Icc a b
⊢ (↑(image (α := 𝕜) (⇑(affineHomeomorph (b - a) a ⋯) : (a : 𝕜) → 𝕜) (Icc 0 1)) : Type u_1) ≃ₜ (↑(Icc a b) : Type u_1)

Tactic:
apply Homeomorph.setCongr

Premises used: Homeomorph.setCongr
-- Module: Mathlib.Topology.UnitInterval
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : IsTopologicalRing 𝕜
a b : 𝕜
h : a < b
e : (↑(Icc 0 1) : Type u_1) ≃ₜ
  (↑(image (α := 𝕜) (⇑(affineHomeomorph (b - a) a ⋯) : (a : 𝕜) → 𝕜) (Icc 0 1)) : Type u_1) :=
  Homeomorph.image (affineHomeomorph (b - a) a ⋯) (Icc 0 1)
h₁ : Icc a (b - a + a) = Icc a b
⊢ image (α := 𝕜) (⇑(affineHomeomorph (b - a) a ⋯) : (a : 𝕜) → 𝕜) (Icc 0 1) = Icc a b

Tactic:
rw [affineHomeomorph_image_I _ _ (sub_pos.2 h)]

Premises used: Iff.mpr, sub_pos, affineHomeomorph_image_I
-- Module: Mathlib.Topology.UnitInterval
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : IsTopologicalRing 𝕜
a b : 𝕜
h : a < b
e : (↑(Icc 0 1) : Type u_1) ≃ₜ
  (↑(image (α := 𝕜) (⇑(affineHomeomorph (b - a) a ⋯) : (a : 𝕜) → 𝕜) (Icc 0 1)) : Type u_1) :=
  Homeomorph.image (affineHomeomorph (b - a) a ⋯) (Icc 0 1)
⊢ Icc a (b - a + a) = Icc a b

Tactic:
simp
-- Module: Mathlib.Topology.UnitInterval
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : IsTopologicalRing 𝕜
a b : 𝕜
h : a < b
x : (↑(Icc a b) : Type u_1)
⊢ (↑((iccHomeoI a b h : (a : (↑(Icc a b) : Type u_1)) → (↑(Icc 0 1) : Type u_1)) x) : 𝕜) = ((↑x : 𝕜) - a) / (b - a)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Icc, Set.image, rfl
-- Module: Mathlib.Topology.UnitInterval
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : IsTopologicalRing 𝕜
a b : 𝕜
h : a < b
x : (↑(Icc 0 1) : Type u_1)
⊢ (↑((Homeomorph.symm (iccHomeoI a b h) : (a_1 : (↑(Icc 0 1) : Type u_1)) → (↑(Icc a b) : Type u_1)) x) : 𝕜) =
    (b - a) * (↑x : 𝕜) + a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UnitInterval
Goal:
⊢ toNNReal 0 = 0

Tactic:
rfl

Premises used: unitInterval.toNNReal, NNReal.mk, rfl
-- Module: Mathlib.Topology.UnitInterval
Goal:
⊢ toNNReal 1 = 1

Tactic:
rfl

Premises used: unitInterval.toNNReal, NNReal.mk, rfl
-- Module: Mathlib.Topology.UnitInterval
Goal:
⊢ Continuous (Y := ℝ≥0) fun (i : (↑I : Type)) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (↑i : ℝ) ⋯

Tactic:
fun_prop
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ (↑(toNNReal x) : ℝ) = (↑x : ℝ)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Icc, NNReal.toReal, rfl
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
a : (↑(toNNReal x + toNNReal (σ x)) : ℝ) = (↑1 : ℝ)
⊢ toNNReal x + toNNReal (σ x) = 1

Tactic:
ext
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ (↑(toNNReal x + toNNReal (σ x)) : ℝ) = (↑1 : ℝ)

Tactic:
simp