awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
t : TopologicalSpace X
inst : CompletelyRegularSpace X
⊢ ∃ (u : UniformSpace X), toTopologicalSpace = t

Tactic:
⟨uniformSpaceOfCompactR1.comap stoneCechUnit, isInducing_stoneCechUnit.eq_induced.symm⟩

Premises used: isInducing_stoneCechUnit, uniformSpaceOfCompactR1, stoneCechUnit, Exists.intro, UniformSpace.comap, Eq.symm, Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
t : TopologicalSpace X
⊢ CompletelyRegularSpace X ↔ ∃ (u : UniformSpace X), toTopologicalSpace = t

Tactic:
⟨(·.exists_uniformSpace), .of_exists_uniformSpace⟩

Premises used: CompletelyRegularSpace.exists_uniformSpace, CompletelyRegularSpace.of_exists_uniformSpace, Iff.intro
-- Module: Mathlib.Topology.UnitInterval
Goal:
⊢ 0 ∈ I

Tactic:
⟨le_rfl, zero_le_one⟩

Premises used: le_rfl, Set.Mem, setOf, zero_le_one, Set.Icc, And.intro
-- Module: Mathlib.Topology.UnitInterval
Goal:
⊢ 1 ∈ I

Tactic:
⟨zero_le_one, le_rfl⟩

Premises used: le_rfl, Set.Mem, setOf, zero_le_one, Set.Icc, And.intro
-- Module: Mathlib.Topology.UnitInterval
Goal:
x y : ℝ
hx : x ∈ I
hy : y ∈ I
⊢ x * y ∈ I

Tactic:
⟨mul_nonneg hx.1 hy.1, mul_le_one₀ hx.2 hy.1 hy.2⟩

Premises used: mul_nonneg, Set.Mem, setOf, Set.Icc, And.right, And.left, mul_le_one₀, And.intro
-- Module: Mathlib.Topology.UnitInterval
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hxy : x ≤ y
⊢ x / y ∈ I

Tactic:
⟨div_nonneg hx hy, div_le_one_of_le₀ hxy hy⟩

Premises used: div_le_one_of_le₀, Set.Mem, setOf, Set.Icc, And.intro, div_nonneg
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : ℝ
⊢ fract x ∈ I

Tactic:
⟨fract_nonneg _, (fract_lt_one _).le⟩

Premises used: Set.Mem, setOf, LT.lt.le, Set.Icc, And.intro, Int.fract_lt_one, Int.fract_nonneg
-- Module: Mathlib.Topology.UnitInterval
Goal:
⊢ Eq (α := Set (↑I : Type)) univ (Icc 0 1)

Tactic:
Icc_bot_top.symm

Premises used: Set.Mem, Set.Icc_bot_top, Eq.symm
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ (↑x : ℝ) ≠ 0 ↔ x ≠ 0

Tactic:
coe_eq_zero.not

Premises used: Iff.not, Set.Icc.coe_eq_zero
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ (↑x : ℝ) ≠ 1 ↔ x ≠ 1

Tactic:
coe_eq_one.not

Premises used: Iff.not, Set.Icc.coe_eq_one
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ 0 < (↑x : ℝ) ↔ 0 < x

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ (↑x : ℝ) < 1 ↔ x < 1

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.UnitInterval
Goal:
x y : (↑I : Type)
⊢ x * y ≤ x

Tactic:
Subtype.coe_le_coe.mp <| mul_le_of_le_one_right x.2.1 y.2.2

Premises used: Subtype.coe_le_coe, mul_le_of_le_one_right, And.right, And.left, Iff.mp, Subtype.property
-- Module: Mathlib.Topology.UnitInterval
Goal:
x y : (↑I : Type)
⊢ x * y ≤ y

Tactic:
Subtype.coe_le_coe.mp <| mul_le_of_le_one_left y.2.1 x.2.2

Premises used: Subtype.coe_le_coe, mul_le_of_le_one_left, And.right, And.left, Iff.mp, Subtype.property
-- Module: Mathlib.Topology.UnitInterval
Goal:
⊢ I = Metric.closedBall 2⁻¹ 2⁻¹

Tactic:
norm_num [unitInterval, Real.Icc_eq_closedBall]

Premises used: Real.Icc_eq_closedBall, unitInterval
-- Module: Mathlib.Topology.UnitInterval
Goal:
⊢ (↑(σ 0) : ℝ) = (↑1 : ℝ)

Tactic:
simp [symm]

Premises used: unitInterval.symm
-- Module: Mathlib.Topology.UnitInterval
Goal:
⊢ (↑(σ 1) : ℝ) = (↑0 : ℝ)

Tactic:
simp [symm]

Premises used: unitInterval.symm
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ (↑(σ (σ x)) : ℝ) = (↑x : ℝ)

Tactic:
simp [symm]

Premises used: unitInterval.symm
-- Module: Mathlib.Topology.UnitInterval
Goal:
⊢ Function.Involutive σ

Tactic:
symm_symm

Premises used: unitInterval.symm_symm, Function.Involutive
-- Module: Mathlib.Topology.UnitInterval
Goal:
⊢ Function.Bijective σ

Tactic:
symm_involutive.bijective

Premises used: Function.Involutive.bijective, unitInterval.symm_involutive
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ (↑(σ x) : ℝ) = 1 - (↑x : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UnitInterval
Goal:
s : Set (↑I : Type)
⊢ Subtype.val (p := fun (x : ℝ) ↦ x ∈ I) '' σ ⁻¹' s =
    (fun (x : ℝ) ↦ 1 - x) ⁻¹' Subtype.val (p := fun (x : ℝ) ↦ x ∈ I) '' s

Tactic:
simp [symm_involutive, ← Function.Involutive.image_eq_preimage_symm, image_image]

Premises used: Set.image_image, unitInterval.symm_involutive, Function.Involutive.image_eq_preimage_symm
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : ℝ
a : (↑(σ (projIcc 0 1 ⋯ x)) : ℝ) = (↑(projIcc 0 1 ⋯ (1 - x)) : ℝ)
⊢ σ (projIcc 0 1 ⋯ x) = projIcc 0 1 ⋯ (1 - x)

Tactic:
ext
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : ℝ
a : ∀ (h₀ : x ≤ 0), (↑(σ (projIcc 0 1 ⋯ x)) : ℝ) = (↑(projIcc 0 1 ⋯ (1 - x)) : ℝ)
a₁ : ∀ (h₀ : 0 ≤ x), (↑(σ (projIcc 0 1 ⋯ x)) : ℝ) = (↑(projIcc 0 1 ⋯ (1 - x)) : ℝ)
⊢ (↑(σ (projIcc 0 1 ⋯ x)) : ℝ) = (↑(projIcc 0 1 ⋯ (1 - x)) : ℝ)

Tactic:
rcases le_total x 0 with h₀ | h₀

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : ℝ
h₀ : x ≤ 0
⊢ (↑(σ (projIcc 0 1 ⋯ x)) : ℝ) = (↑(projIcc 0 1 ⋯ (1 - x)) : ℝ)

Tactic:
simp [projIcc_of_le_left, projIcc_of_right_le, h₀]

Premises used: Set.projIcc_of_right_le, Set.projIcc_of_le_left
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : ℝ
h₀ : 0 ≤ x
a : ∀ (h₁ : x ≤ 1), (↑(σ (projIcc 0 1 ⋯ x)) : ℝ) = (↑(projIcc 0 1 ⋯ (1 - x)) : ℝ)
a₁ : ∀ (h₁ : 1 ≤ x), (↑(σ (projIcc 0 1 ⋯ x)) : ℝ) = (↑(projIcc 0 1 ⋯ (1 - x)) : ℝ)
⊢ (↑(σ (projIcc 0 1 ⋯ x)) : ℝ) = (↑(projIcc 0 1 ⋯ (1 - x)) : ℝ)

Tactic:
rcases le_total x 1 with h₁ | h₁

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : ℝ
h₀ : 0 ≤ x
h₁ : x ≤ 1
⊢ x ∈ I

Tactic:
⟨h₀, h₁⟩

Premises used: Set.Mem, setOf, Set.Icc, And.intro
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : ℝ
h₀ : 0 ≤ x
h₁ : x ≤ 1
a :
  ∀ (x : { x : ℝ // x ∈ I }) (h₀ : 0 ≤ (↑x : ℝ)) (h₁ : (↑x : ℝ) ≤ 1),
    (↑(σ (projIcc 0 1 ⋯ (↑x : ℝ))) : ℝ) = (↑(projIcc 0 1 ⋯ (1 - (↑x : ℝ))) : ℝ)
⊢ (↑(σ (projIcc 0 1 ⋯ x)) : ℝ) = (↑(projIcc 0 1 ⋯ (1 - x)) : ℝ)

Tactic:
lift x to I using ⟨h₀, h₁⟩
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : ℝ
h₀ : 0 ≤ x
h₁ : 1 ≤ x
⊢ (↑(σ (projIcc 0 1 ⋯ x)) : ℝ) = (↑(projIcc 0 1 ⋯ (1 - x)) : ℝ)

Tactic:
simp [projIcc_of_le_left, projIcc_of_right_le, h₁]

Premises used: Set.projIcc_of_right_le, Set.projIcc_of_le_left
-- Module: Mathlib.Topology.UnitInterval
Goal:
⊢ Continuous (Y := ℝ) fun (x : (↑I : Type)) ↦ 1 - (↑x : ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Topology.UnitInterval
Goal:
⊢ StrictAnti σ

Tactic:
fun _ _ h ↦ sub_lt_sub_left (α := ℝ) h _

Premises used: StrictAnti, OfNat.ofNat, sub_lt_sub_left
-- Module: Mathlib.Topology.UnitInterval
Goal:
i j : (↑I : Type)
⊢ σ i = σ j ↔ i = j

Tactic:
symm_bijective.injective.eq_iff

Premises used: Function.Injective.eq_iff, Function.Bijective.injective, unitInterval.symm_bijective
-- Module: Mathlib.Topology.UnitInterval
Goal:
t : (↑I : Type)
rw : 1 / 2 ≤ 1 - (↑t : ℝ) ↔ (↑t : ℝ) ≤ 1 / 2
rw₁ : 1 / 2 + (↑t : ℝ) ≤ 1 ↔ (↑t : ℝ) ≤ 1 / 2
rw₂ : (↑t : ℝ) + 1 / 2 ≤ 1 ↔ (↑t : ℝ) ≤ 1 / 2
rw₃ : (↑t : ℝ) ≤ 1 - 1 / 2 ↔ (↑t : ℝ) ≤ 1 / 2
rw₄ rw₅ : (↑t : ℝ) ≤ 1 / 2 ↔ (↑t : ℝ) ≤ 1 / 2
⊢ 1 / 2 ≤ (↑(σ t) : ℝ) ↔ (↑t : ℝ) ≤ 1 / 2

Tactic:
rw [coe_symm_eq, le_sub_iff_add_le, add_comm, ← le_sub_iff_add_le, sub_half]

Premises used: unitInterval.coe_symm_eq, add_comm, le_sub_iff_add_le, sub_half
-- Module: Mathlib.Topology.UnitInterval
Goal:
i : (↑I : Type)
rw : σ i = σ 0 ↔ i = 0
rw₁ rw₂ : i = 0 ↔ i = 0
⊢ σ i = 1 ↔ i = 0

Tactic:
rw [← symm_zero, symm_inj]

Premises used: unitInterval.symm_inj, unitInterval.symm_zero
-- Module: Mathlib.Topology.UnitInterval
Goal:
i : (↑I : Type)
rw : σ i = σ 1 ↔ i = 1
rw₁ rw₂ : i = 1 ↔ i = 1
⊢ σ i = 0 ↔ i = 1

Tactic:
rw [← symm_one, symm_inj]

Premises used: unitInterval.symm_one, unitInterval.symm_inj
-- Module: Mathlib.Topology.UnitInterval
Goal:
i j : (↑I : Type)
⊢ σ i ≤ σ j ↔ j ≤ i

Tactic:
simp only [symm, Subtype.mk_le_mk, sub_le_sub_iff, add_le_add_iff_left, Subtype.coe_le_coe]

Premises used: add_le_add_iff_left, Subtype.coe_le_coe, sub_le_sub_iff, unitInterval.symm, Subtype.mk_le_mk
-- Module: Mathlib.Topology.UnitInterval
Goal:
i j : (↑I : Type)
rw : σ (σ j) ≤ σ i ↔ j ≤ σ i
rw₁ rw₂ : j ≤ σ i ↔ j ≤ σ i
⊢ i ≤ σ j ↔ j ≤ σ i

Tactic:
rw [← symm_le_symm, symm_symm]

Premises used: unitInterval.symm_le_symm, unitInterval.symm_symm
-- Module: Mathlib.Topology.UnitInterval
Goal:
i j : (↑I : Type)
rw : σ j ≤ σ (σ i) ↔ σ j ≤ i
rw₁ rw₂ : σ j ≤ i ↔ σ j ≤ i
⊢ σ i ≤ j ↔ σ j ≤ i

Tactic:
rw [← symm_le_symm, symm_symm]

Premises used: unitInterval.symm_le_symm, unitInterval.symm_symm
-- Module: Mathlib.Topology.UnitInterval
Goal:
i j : (↑I : Type)
⊢ σ i < σ j ↔ j < i

Tactic:
simp only [symm, Subtype.mk_lt_mk, sub_lt_sub_iff_left, Subtype.coe_lt_coe]

Premises used: Subtype.coe_lt_coe, Subtype.mk_lt_mk, sub_lt_sub_iff_left, unitInterval.symm
-- Module: Mathlib.Topology.UnitInterval
Goal:
i j : (↑I : Type)
rw : σ (σ j) < σ i ↔ j < σ i
rw₁ rw₂ : j < σ i ↔ j < σ i
⊢ i < σ j ↔ j < σ i

Tactic:
rw [← symm_lt_symm, symm_symm]

Premises used: unitInterval.symm_symm, unitInterval.symm_lt_symm
-- Module: Mathlib.Topology.UnitInterval
Goal:
i j : (↑I : Type)
rw : σ j < σ (σ i) ↔ σ j < i
rw₁ rw₂ : σ j < i ↔ σ j < i
⊢ σ i < j ↔ σ j < i

Tactic:
rw [← symm_lt_symm, symm_symm]

Premises used: unitInterval.symm_symm, unitInterval.symm_lt_symm
-- Module: Mathlib.Topology.UnitInterval
Goal:
⊢ ConnectedSpace (↑I : Type)

Tactic:
Subtype.connectedSpace ⟨nonempty_Icc.mpr zero_le_one, isPreconnected_Icc⟩

Premises used: Iff.mpr, Set.nonempty_Icc, isPreconnected_Icc, Subtype.connectedSpace, zero_le_one, And.intro
-- Module: Mathlib.Topology.UnitInterval
Goal:
⊢ CompactSpace (↑I : Type)

Tactic:
infer_instance
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ 0 ≤ (↑x : ℝ)

Tactic:
x.2.1

Premises used: And.left, Subtype.property
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ 0 ≤ 1 - (↑x : ℝ)

Tactic:
simpa using x.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ (↑x : ℝ) ≤ 1

Tactic:
x.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ 1 - (↑x : ℝ) ≤ 1

Tactic:
simpa using x.2.1

Premises used: And.left, Subtype.property
-- Module: Mathlib.Topology.UnitInterval
Goal:
t : (↑I : Type)
x : ℝ
hx : 0 < x
⊢ 0 < x + (↑t : ℝ)

Tactic:
add_pos_of_pos_of_nonneg hx <| nonneg _

Premises used: unitInterval.nonneg, add_pos_of_pos_of_nonneg
-- Module: Mathlib.Topology.UnitInterval
Goal:
t : (↑I : Type)
⊢ 0 ≤ t

Tactic:
t.2.1

Premises used: And.left, Subtype.property
-- Module: Mathlib.Topology.UnitInterval
Goal:
t : (↑I : Type)
⊢ t ≤ 1

Tactic:
t.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ 0 < x ↔ x ≠ 0

Tactic:
bot_lt_iff_ne_bot

Premises used: Set.Mem, bot_lt_iff_ne_bot
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ x < 1 ↔ x ≠ 1

Tactic:
lt_top_iff_ne_top

Premises used: Set.Mem, lt_top_iff_ne_top
-- Module: Mathlib.Topology.UnitInterval
Goal:
i j : (↑I : Type)
h : i ≤ j * i
contrapose! : ∀ (h : i ≠ 0 ∧ j ≠ 1), j * i < i
⊢ i = 0 ∨ j = 1

Tactic:
contrapose! h
-- Module: Mathlib.Topology.UnitInterval
Goal:
i j : (↑I : Type)
h : i ≠ 0 ∧ j ≠ 1
⊢ 0 < (↑i : ℝ) ∧ (↑j : ℝ) < 1

Tactic:
rw [← unitInterval.lt_one_iff_ne_one, ← coe_lt_one, ← unitInterval.pos_iff_ne_zero,
    ← coe_pos] at h

Premises used: unitInterval.pos_iff_ne_zero, unitInterval.lt_one_iff_ne_one, unitInterval.coe_lt_one, unitInterval.coe_pos
-- Module: Mathlib.Topology.UnitInterval
Goal:
i j : (↑I : Type)
h : 0 < (↑i : ℝ) ∧ (↑j : ℝ) < 1
⊢ (↑j : ℝ) * (↑i : ℝ) < (↑i : ℝ)

Tactic:
simpa using mul_lt_mul_of_pos_right h.right h.left

Premises used: mul_lt_mul_of_pos_right, And.right, And.left
-- Module: Mathlib.Topology.UnitInterval
Goal:
⊢ Nontrivial (↑I : Type)

Tactic:
⟨⟨1, 0, (one_ne_zero <| congrArg Subtype.val ·)⟩⟩

Premises used: congrArg, Nontrivial.mk, Exists.intro, one_ne_zero, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Topology.UnitInterval
Goal:
a t : ℝ
ha : 0 < a
mp : a * t ∈ I → t ∈ Icc 0 (1 / a)
mpr : t ∈ Icc 0 (1 / a) → a * t ∈ I
⊢ a * t ∈ I ↔ t ∈ Icc 0 (1 / a)

Tactic:
constructor
-- Module: Mathlib.Topology.UnitInterval
Goal:
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
mp : 0 ≤ t
mp₁ : t ≤ 1 / a
⊢ t ∈ Icc 0 (1 / a)

Tactic:
constructor
-- Module: Mathlib.Topology.UnitInterval
Goal:
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
mpr : 0 ≤ a * t
mpr₁ : a * t ≤ 1
⊢ a * t ∈ I

Tactic:
constructor
-- Module: Mathlib.Topology.UnitInterval
Goal:
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ 0 ≤ t

Tactic:
nonneg_of_mul_nonneg_right h₁ ha

Premises used: nonneg_of_mul_nonneg_right
-- Module: Mathlib.Topology.UnitInterval
Goal:
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ 0 ≤ t

Tactic:
exact nonneg_of_mul_nonneg_right h₁ ha

Premises used: nonneg_of_mul_nonneg_right
-- Module: Mathlib.Topology.UnitInterval
Goal:
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
mp : t * a ≤ 1
mp₁ mp₂ mp₃ mp₄ : a * t ≤ 1
⊢ t ≤ 1 / a

Tactic:
rwa [le_div_iff₀ ha, mul_comm]

Premises used: mul_comm, le_div_iff₀
-- Module: Mathlib.Topology.UnitInterval
Goal:
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ 0 ≤ a * t

Tactic:
mul_nonneg ha.le h₁

Premises used: mul_nonneg, LT.lt.le
-- Module: Mathlib.Topology.UnitInterval
Goal:
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ 0 ≤ a * t

Tactic:
exact mul_nonneg ha.le h₁

Premises used: mul_nonneg, LT.lt.le
-- Module: Mathlib.Topology.UnitInterval
Goal:
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
mpr : ∀ (h₂ : t * a ≤ 1), a * t ≤ 1
mpr₁ mpr₂ mpr₃ mpr₄ : ∀ (h₂ : a * t ≤ 1), a * t ≤ 1
⊢ a * t ≤ 1

Tactic:
rwa [le_div_iff₀ ha, mul_comm] at h₂

Premises used: mul_comm, le_div_iff₀
-- Module: Mathlib.Topology.UnitInterval
Goal:
t : ℝ
mp : 2 * t - 1 ∈ I → t ∈ Icc (1 / 2) 1
mpr : t ∈ Icc (1 / 2) 1 → 2 * t - 1 ∈ I
⊢ 2 * t - 1 ∈ I ↔ t ∈ Icc (1 / 2) 1

Tactic:
constructor
-- Module: Mathlib.Topology.UnitInterval
Goal:
t : ℝ
h₁ : 0 ≤ 2 * t - 1
h₂ : 2 * t - 1 ≤ 1
mp : 1 / 2 ≤ t
mp₁ : t ≤ 1
⊢ t ∈ Icc (1 / 2) 1

Tactic:
constructor
-- Module: Mathlib.Topology.UnitInterval
Goal:
t : ℝ
h₁ : 1 / 2 ≤ t
h₂ : t ≤ 1
mpr : 0 ≤ 2 * t - 1
mpr₁ : 2 * t - 1 ≤ 1
⊢ 2 * t - 1 ∈ I

Tactic:
constructor
-- Module: Mathlib.Topology.UnitInterval
Goal:
t : ℝ
h₁ : 0 ≤ 2 * t - 1
h₂ : 2 * t - 1 ≤ 1
linarith : t < 1 / 2 → 2 / 2 = 1
linarith₁ : t < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : t < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : t < 1 / 2 → 0 - (2 * t - 1) + (2 * t - HMul.hMul (α := ℝ) 1 1) = 0
⊢ 1 / 2 ≤ t

Tactic:
linarith
-- Module: Mathlib.Topology.UnitInterval
Goal:
t : ℝ
h₁ : 0 ≤ 2 * t - 1
h₂ : 2 * t - 1 ≤ 1
linarith : 1 < t → 2 * t - 1 - 1 + 2 * (1 - t) = 0
linarith₁ : 1 < t → GT.gt (α := ℝ) 2 0
⊢ t ≤ 1

Tactic:
linarith
-- Module: Mathlib.Topology.UnitInterval
Goal:
t : ℝ
h₁ : 1 / 2 ≤ t
h₂ : t ≤ 1
linarith : 2 * t - 1 < 0 → 2 / 2 = 1
linarith₁ : 2 * t - 1 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2 * t - 1 < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : 2 * t - 1 < 0 → HMul.hMul (α := ℝ) 1 1 - 2 * t + (2 * t - 1 - 0) = 0
⊢ 0 ≤ 2 * t - 1

Tactic:
linarith
-- Module: Mathlib.Topology.UnitInterval
Goal:
t : ℝ
h₁ : 1 / 2 ≤ t
h₂ : t ≤ 1
linarith : 1 < 2 * t - 1 → 2 / 2 = 1
linarith₁ : 1 < 2 * t - 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 < 2 * t - 1 → GT.gt (α := ℝ) 2 0
linarith₃ : 1 < 2 * t - 1 → 2 * (t - 1) + (1 - (2 * t - 1)) = 0
linarith₄ : 1 < 2 * t - 1 → GT.gt (α := ℝ) 2 0
⊢ 2 * t - 1 ≤ 1

Tactic:
linarith
-- Module: Mathlib.Topology.UnitInterval
Goal:
⊢ (↑submonoid : Set ℝ) = I

Tactic:
rfl

Premises used: setOf, Set.Icc, rfl
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : ℝ
⊢ x ∈ submonoid ↔ x ∈ I

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Icc
-- Module: Mathlib.Topology.UnitInterval
Goal:
ι : Type u_1
t : Finset ι
f : ι → ℝ
h : ∀ c ∈ t, f c ∈ I
⊢ ∏ c ∈ t, f c ∈ I

Tactic:
_root_.prod_mem (S := unitInterval.submonoid) h

Premises used: Set.Mem, setOf, Set.Icc, prod_mem
-- Module: Mathlib.Topology.UnitInterval
Goal:
i : (↑I : Type)
hi : 0 < i
j k : (↑I : Type)
hjk : j < k
ha : 0 < (↑i : ℝ)
⊢ (↑i : ℝ) * (↑j : ℝ) < (↑i : ℝ) * (↑k : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ Iic x = Icc 0 x

Tactic:
Icc_bot.symm

Premises used: Set.Mem, Set.Icc_bot, Eq.symm
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ Iic x = Icc 0 x

Tactic:
exact Icc_bot.symm

Premises used: Set.Icc_bot, Eq.symm
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ Iio x = Ico 0 x

Tactic:
Ico_bot.symm

Premises used: Set.Mem, Set.Ico_bot, Eq.symm
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ Iio x = Ico 0 x

Tactic:
exact Ico_bot.symm

Premises used: Set.Ico_bot, Eq.symm
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ Ici x = Icc x 1

Tactic:
Icc_top.symm

Premises used: Set.Mem, Set.Icc_top, Eq.symm
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ Ici x = Icc x 1

Tactic:
exact Icc_top.symm

Premises used: Set.Icc_top, Eq.symm
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ Ioi x = Ioc x 1

Tactic:
Ioc_top.symm

Premises used: Set.Ioc_top, Set.Mem, Eq.symm
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ Ioi x = Ioc x 1

Tactic:
exact Ioc_top.symm

Premises used: Set.Ioc_top, Eq.symm
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
inr :
  ∀ (this : ∀ {c d : α} (hdc : d ≤ c), |(↑(projIcc a b h c) : α) - (↑(projIcc a b h d) : α)| ≤ |c - d|) (hdc : ¬d ≤ c),
    |(↑(projIcc a b h c) : α) - (↑(projIcc a b h d) : α)| ≤ |c - d|
wlog : ∀ {c d : α} (hdc : d ≤ c), |(↑(projIcc a b h c) : α) - (↑(projIcc a b h d) : α)| ≤ |c - d|
⊢ |(↑(projIcc a b h c) : α) - (↑(projIcc a b h d) : α)| ≤ |c - d|

Tactic:
wlog hdc : d ≤ c generalizing c d
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
this : ∀ {c d : α} (hdc : d ≤ c), |(↑(projIcc a b h c) : α) - (↑(projIcc a b h d) : α)| ≤ |c - d|
hdc : ¬d ≤ c
inr : |(↑(projIcc a b h d) : α) - (↑(projIcc a b h c) : α)| ≤ |d - c|
⊢ |(↑(projIcc a b h c) : α) - (↑(projIcc a b h d) : α)| ≤ |c - d|

Tactic:
rw [abs_sub_comm, abs_sub_comm c]

Premises used: abs_sub_comm
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
this : ∀ {c d : α} (hdc : d ≤ c), |(↑(projIcc a b h c) : α) - (↑(projIcc a b h d) : α)| ≤ |c - d|
hdc : ¬d ≤ c
⊢ |(↑(projIcc a b h d) : α) - (↑(projIcc a b h c) : α)| ≤ |d - c|

Tactic:
this (le_of_not_ge hdc)

Premises used: le_of_not_ge
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
this : ∀ {c d : α} (hdc : d ≤ c), |(↑(projIcc a b h c) : α) - (↑(projIcc a b h d) : α)| ≤ |c - d|
hdc : ¬d ≤ c
⊢ |(↑(projIcc a b h d) : α) - (↑(projIcc a b h c) : α)| ≤ |d - c|

Tactic:
exact this (le_of_not_ge hdc)

Premises used: le_of_not_ge
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c_1 d_1 : α
h : a ≤ b
c d : α
hdc : d ≤ c
rw : (↑(projIcc a b h c) : α) - (↑(projIcc a b h d) : α) ≤ c - d
⊢ |(↑(projIcc a b h c) : α) - (↑(projIcc a b h d) : α)| ≤ |c - d|

Tactic:
rw [abs_eq_self.2 (sub_nonneg.2 hdc),
    abs_eq_self.2 (sub_nonneg.2 <| mod_cast monotone_projIcc h hdc)]

Premises used: Iff.mpr, sub_nonneg, abs_eq_self
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c_1 d_1 : α
h : a ≤ b
c d : α
hdc : d ≤ c
⊢ 0 ≤ c - d

Tactic:
rw [← sub_nonneg] at hdc

Premises used: sub_nonneg
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c_1 d_1 : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
rwa rwa₁ rwa₂ rwa₃ : 0 ≤ c - d
⊢ a - a ≤ c - d

Tactic:
rwa [sub_self]

Premises used: sub_self
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c_1 d_1 : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
refine : min b c - min b d ≤ c - d
⊢ (↑(projIcc a b h c) : α) - (↑(projIcc a b h d) : α) ≤ c - d

Tactic:
refine (max_sub_max_le_max _ _ _ _).trans (max_le (by rwa [sub_self]) ?_)

Premises used: max_sub_max_le_max, max_le, LE.le.trans
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c_1 d_1 : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
⊢ min b c - min b d ≤ c - d

Tactic:
((le_abs_self _).trans <| abs_min_sub_min_le_max _ _ _ _).trans (max_le ?_ ?_)

Premises used: le_abs_self, max_le, LE.le.trans, abs_min_sub_min_le_max
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c_1 d_1 : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
refine_1 : |b - b| ≤ c - d
refine_2 : |c - d| ≤ c - d
⊢ min b c - min b d ≤ c - d

Tactic:
refine ((le_abs_self _).trans <| abs_min_sub_min_le_max _ _ _ _).trans (max_le ?_ ?_)

Premises used: le_abs_self, max_le, LE.le.trans, abs_min_sub_min_le_max
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c_1 d_1 : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
refine_1 : |0| ≤ c - d
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : 0 ≤ c - d
⊢ |b - b| ≤ c - d

Tactic:
rwa [sub_self, abs_zero]

Premises used: sub_self, abs_zero
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c_1 d_1 : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
⊢ |c - d| ≤ c - d

Tactic:
(abs_eq_self.mpr hdc).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 c_1 d_1 : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
⊢ |c - d| ≤ c - d

Tactic:
exact (abs_eq_self.mpr hdc).le

Premises used: Iff.mpr, Eq.le, abs_eq_self
-- Module: Mathlib.Topology.UnitInterval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : α
h : a ≤ b
δ : α
rw : (↑(projIcc a b h (a + HSMul.hSMul (α := ℕ) 0 δ)) : α) = a
rw₁ : (↑(projIcc a b h (a + 0)) : α) = a
rw₂ : (↑(projIcc a b h a) : α) = a
rw₃ rw₄ : (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a ⋯) : α) = a
⊢ (↑(addNSMul h δ 0) : α) = a

Tactic:
rw [addNSMul, zero_smul, add_zero, projIcc_left]

Premises used: Set.projIcc_left, Set.Icc.addNSMul, zero_smul, add_zero
-- 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 < δ
obtain : ∀ (m : ℕ) (hm : b - a ≤ m • δ), ∃ (m : ℕ), ∀ n ≥ m, (↑(addNSMul h δ n) : α) = b
⊢ ∃ (m : ℕ), ∀ n ≥ m, (↑(addNSMul h δ n) : α) = b

Tactic:
obtain ⟨m, hm⟩ := Archimedean.arch (b - a) hδ

Premises used: HSub.hSub, Archimedean.arch
-- 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 • δ
⊢ ∃ (m : ℕ), ∀ n ≥ m, (↑(addNSMul h δ n) : α) = b

Tactic:
⟨m, fun n hn ↦ ?_⟩

Premises used: Exists.intro
-- 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 • δ
refine : ∀ (n : ℕ) (hn : n ≥ m), (↑(addNSMul h δ n) : α) = b
⊢ ∃ (m : ℕ), ∀ n ≥ m, (↑(addNSMul h δ n) : α) = b

Tactic:
refine ⟨m, fun n hn ↦ ?_⟩