awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
i : (↑I : Type)
⊢ σ i = 0 ↔ i = 1
have rw : σ i = σ 1 ↔ i = 1
Tactic: rw [← symm_one, symm_inj]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
i : (↑I : Type)
rw : σ i = σ 1 ↔ i = 1
⊢ σ i = 0 ↔ i = 1
have rw₁ : i = 1 ↔ i = 1
Tactic: rw [← symm_one, symm_inj]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
i j : (↑I : Type)
⊢ i ≤ σ j ↔ j ≤ σ i
have rw : σ (σ j) ≤ σ i ↔ j ≤ σ i
Tactic: rw [← symm_le_symm, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
i j : (↑I : Type)
rw : σ (σ j) ≤ σ i ↔ j ≤ σ i
⊢ i ≤ σ j ↔ j ≤ σ i
have rw₁ : j ≤ σ i ↔ j ≤ σ i
Tactic: rw [← symm_le_symm, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
i j : (↑I : Type)
⊢ σ i ≤ j ↔ σ j ≤ i
have rw : σ j ≤ σ (σ i) ↔ σ j ≤ i
Tactic: rw [← symm_le_symm, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
i j : (↑I : Type)
rw : σ j ≤ σ (σ i) ↔ σ j ≤ i
⊢ σ i ≤ j ↔ σ j ≤ i
have rw₁ : σ j ≤ i ↔ σ j ≤ i
Tactic: rw [← symm_le_symm, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
i j : (↑I : Type)
⊢ i < σ j ↔ j < σ i
have rw : σ (σ j) < σ i ↔ j < σ i
Tactic: rw [← symm_lt_symm, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
i j : (↑I : Type)
rw : σ (σ j) < σ i ↔ j < σ i
⊢ i < σ j ↔ j < σ i
have rw₁ : j < σ i ↔ j < σ i
Tactic: rw [← symm_lt_symm, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
i j : (↑I : Type)
⊢ σ i < j ↔ σ j < i
have rw : σ j < σ (σ i) ↔ σ j < i
Tactic: rw [← symm_lt_symm, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
i j : (↑I : Type)
rw : σ j < σ (σ i) ↔ σ j < i
⊢ σ i < j ↔ σ j < i
have rw₁ : σ j < i ↔ σ j < i
Tactic: rw [← symm_lt_symm, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
i j : (↑I : Type)
h : i ≤ j * i
⊢ i = 0 ∨ j = 1
have contrapose! : ∀ (h : i ≠ 0 ∧ j ≠ 1), j * i < i
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (hypothesis)
Goal:
i j : (↑I : Type)
h : i ≠ 0 ∧ j ≠ 1
⊢ j * i < i
have h₁ : 0 < (↑i : ℝ) ∧ (↑j : ℝ) < 1
Tactic: rw [← unitInterval.lt_one_iff_ne_one, ← coe_lt_one, ← unitInterval.pos_iff_ne_zero,
    ← coe_pos] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a t : ℝ
ha : 0 < a
⊢ a * t ∈ I ↔ t ∈ Icc 0 (1 / a)
have mp : a * t ∈ I → t ∈ Icc 0 (1 / a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a t : ℝ
ha : 0 < a
mp : a * t ∈ I → t ∈ Icc 0 (1 / a)
⊢ a * t ∈ I ↔ t ∈ Icc 0 (1 / a)
have mpr : t ∈ Icc 0 (1 / a) → a * t ∈ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ t ∈ Icc 0 (1 / a)
have mp : 0 ≤ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
mp : 0 ≤ t
⊢ t ∈ Icc 0 (1 / a)
have mp₁ : t ≤ 1 / a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ a * t ∈ I
have mpr : 0 ≤ a * t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
mpr : 0 ≤ a * t
⊢ a * t ∈ I
have mpr₁ : a * t ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ t ≤ 1 / a
have mp : t * a ≤ 1
Tactic: rwa [le_div_iff₀ ha, mul_comm]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ a * t ≤ 1
have mpr : ∀ (h₂ : t * a ≤ 1), a * t ≤ 1
Tactic: rwa [le_div_iff₀ ha, mul_comm] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
mpr : ∀ (h₂ : t * a ≤ 1), a * t ≤ 1
⊢ a * t ≤ 1
have mpr₁ : ∀ (h₂ : a * t ≤ 1), a * t ≤ 1
Tactic: rwa [le_div_iff₀ ha, mul_comm] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : ℝ
⊢ 2 * t - 1 ∈ I ↔ t ∈ Icc (1 / 2) 1
have mp : 2 * t - 1 ∈ I → t ∈ Icc (1 / 2) 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : ℝ
mp : 2 * t - 1 ∈ I → t ∈ Icc (1 / 2) 1
⊢ 2 * t - 1 ∈ I ↔ t ∈ Icc (1 / 2) 1
have mpr : t ∈ Icc (1 / 2) 1 → 2 * t - 1 ∈ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : ℝ
h₁ : 0 ≤ 2 * t - 1
h₂ : 2 * t - 1 ≤ 1
⊢ t ∈ Icc (1 / 2) 1
have mp : 1 / 2 ≤ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : ℝ
h₁ : 0 ≤ 2 * t - 1
h₂ : 2 * t - 1 ≤ 1
mp : 1 / 2 ≤ t
⊢ t ∈ Icc (1 / 2) 1
have mp₁ : t ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : ℝ
h₁ : 1 / 2 ≤ t
h₂ : t ≤ 1
⊢ 2 * t - 1 ∈ I
have mpr : 0 ≤ 2 * t - 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : ℝ
h₁ : 1 / 2 ≤ t
h₂ : t ≤ 1
mpr : 0 ≤ 2 * t - 1
⊢ 2 * t - 1 ∈ I
have mpr₁ : 2 * t - 1 ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : ℝ
h₁ : 0 ≤ 2 * t - 1
h₂ : 2 * t - 1 ≤ 1
⊢ 1 / 2 ≤ t
have linarith : t < 1 / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : ℝ
h₁ : 0 ≤ 2 * t - 1
h₂ : 2 * t - 1 ≤ 1
linarith : t < 1 / 2 → 2 / 2 = 1
⊢ 1 / 2 ≤ t
have linarith₁ : t < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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
⊢ 1 / 2 ≤ t
have linarith₂ : t < 1 / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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
⊢ 1 / 2 ≤ t
have linarith₃ : t < 1 / 2 → 0 - (2 * t - 1) + (2 * t - HMul.hMul (α := ℝ) 1 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : ℝ
h₁ : 0 ≤ 2 * t - 1
h₂ : 2 * t - 1 ≤ 1
⊢ t ≤ 1
have linarith : 1 < t → 2 * t - 1 - 1 + 2 * (1 - t) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : ℝ
h₁ : 0 ≤ 2 * t - 1
h₂ : 2 * t - 1 ≤ 1
linarith : 1 < t → 2 * t - 1 - 1 + 2 * (1 - t) = 0
⊢ t ≤ 1
have linarith₁ : 1 < t → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : ℝ
h₁ : 1 / 2 ≤ t
h₂ : t ≤ 1
⊢ 0 ≤ 2 * t - 1
have linarith : 2 * t - 1 < 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : ℝ
h₁ : 1 / 2 ≤ t
h₂ : t ≤ 1
linarith : 2 * t - 1 < 0 → 2 / 2 = 1
⊢ 0 ≤ 2 * t - 1
have linarith₁ : 2 * t - 1 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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
⊢ 0 ≤ 2 * t - 1
have linarith₂ : 2 * t - 1 < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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
⊢ 0 ≤ 2 * t - 1
have linarith₃ : 2 * t - 1 < 0 → HMul.hMul (α := ℝ) 1 1 - 2 * t + (2 * t - 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : ℝ
h₁ : 1 / 2 ≤ t
h₂ : t ≤ 1
⊢ 2 * t - 1 ≤ 1
have linarith : 1 < 2 * t - 1 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : ℝ
h₁ : 1 / 2 ≤ t
h₂ : t ≤ 1
linarith : 1 < 2 * t - 1 → 2 / 2 = 1
⊢ 2 * t - 1 ≤ 1
have linarith₁ : 1 < 2 * t - 1 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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
⊢ 2 * t - 1 ≤ 1
have linarith₂ : 1 < 2 * t - 1 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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
⊢ 2 * t - 1 ≤ 1
have linarith₃ : 1 < 2 * t - 1 → 2 * (t - 1) + (1 - (2 * t - 1)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
i : (↑I : Type)
hi : 0 < i
j k : (↑I : Type)
hjk : j < k
⊢ (↑i : ℝ) * (↑j : ℝ) < (↑i : ℝ) * (↑k : ℝ)
have ha : 0 < (↑i : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
⊢ |(↑(projIcc a b h c) : α) - (↑(projIcc a b h d) : α)| ≤ |c - d|
have 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|
Tactic: wlog hdc : d ≤ c generalizing c d
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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|
⊢ |(↑(projIcc a b h c) : α) - (↑(projIcc a b h d) : α)| ≤ |c - d|
have wlog : ∀ {c d : α} (hdc : d ≤ c), |(↑(projIcc a b h c) : α) - (↑(projIcc a b h d) : α)| ≤ |c - d|
Tactic: wlog hdc : d ≤ c generalizing c d
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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 c) : α) - (↑(projIcc a b h d) : α)| ≤ |c - d|
have inr : |(↑(projIcc a b h d) : α) - (↑(projIcc a b h c) : α)| ≤ |d - c|
Tactic: rw [abs_sub_comm, abs_sub_comm c]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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
⊢ |(↑(projIcc a b h c) : α) - (↑(projIcc a b h d) : α)| ≤ |c - d|
have rw : (↑(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)]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (hypothesis)
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
⊢ (↑(projIcc a b h c) : α) - (↑(projIcc a b h d) : α) ≤ c - d
have hdc₁ : 0 ≤ c - d
Tactic: rw [← sub_nonneg] at hdc
Cleared hypotheses: hdc
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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
⊢ (↑(projIcc a b h c) : α) - (↑(projIcc a b h d) : α) ≤ c - d
have refine : min b c - min b d ≤ c - d
Tactic: refine (max_sub_max_le_max _ _ _ _).trans (max_le (by rwa [sub_self]) ?_)
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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
have refine_1 : |b - b| ≤ c - d
Tactic: refine ((le_abs_self _).trans <| abs_min_sub_min_le_max _ _ _ _).trans (max_le ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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
⊢ min b c - min b d ≤ c - d
have refine_2 : |c - d| ≤ c - d
Tactic: refine ((le_abs_self _).trans <| abs_min_sub_min_le_max _ _ _ _).trans (max_le ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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
⊢ |b - b| ≤ c - d
have refine_1 : |0| ≤ c - d
Tactic: rwa [sub_self, abs_zero]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : α
h : a ≤ b
δ : α
⊢ (↑(addNSMul h δ 0) : α) = a
have rw : (↑(projIcc a b h (a + HSMul.hSMul (α := ℕ) 0 δ)) : α) = a
Tactic: rw [addNSMul, zero_smul, add_zero, projIcc_left]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : α
h : a ≤ b
δ : α
rw : (↑(projIcc a b h (a + HSMul.hSMul (α := ℕ) 0 δ)) : α) = a
⊢ (↑(addNSMul h δ 0) : α) = a
have rw₁ : (↑(projIcc a b h (a + 0)) : α) = a
Tactic: rw [addNSMul, zero_smul, add_zero, projIcc_left]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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
⊢ (↑(addNSMul h δ 0) : α) = a
have rw₂ : (↑(projIcc a b h a) : α) = a
Tactic: rw [addNSMul, zero_smul, add_zero, projIcc_left]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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
⊢ (↑(addNSMul h δ 0) : α) = a
have rw₃ : (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a sorry) : α) = a
Tactic: rw [addNSMul, zero_smul, add_zero, projIcc_left]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
inst_3 : Archimedean α
hδ : 0 < δ
⊢ ∃ (m : ℕ), ∀ n ≥ m, (↑(addNSMul h δ n) : α) = b
have obtain : ∀ (m : ℕ) (hm : b - a ≤ m • δ), ∃ (m : ℕ), ∀ n ≥ m, (↑(addNSMul h δ n) : α) = b
Tactic: obtain ⟨m, hm⟩ := Archimedean.arch (b - a) hδ
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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
have refine : ∀ (n : ℕ) (hn : n ≥ m), (↑(addNSMul h δ n) : α) = b
Tactic: refine ⟨m, fun n hn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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
⊢ (↑(addNSMul h δ n) : α) = b
have rw : b ≤ n • δ + a
Tactic: rw [addNSMul, coe_projIcc, add_comm, min_eq_left_iff.mpr, max_eq_right h]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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 : α) - (↑(addNSMul h δ n) : α) ≤ (↑(projIcc a b h (a + (n + 1) • δ)) : α) - (↑(addNSMul h δ n) : α)
have h₁ : (↑t : α) ≤ (↑(projIcc a b h (a + (n + 1) • δ)) : α)
Tactic: apply sub_le_sub_right
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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))
⊢ |a + (n + 1) • δ - (a + n • δ)| ≤ δ
have rw : |δ| ≤ δ
Tactic: rw [add_sub_add_comm, sub_self, zero_add, succ_nsmul', add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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)
⊢ (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) ∈ Icc a b
have left : a ≤ (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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 : ℝ)
⊢ (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) ∈ Icc a b
have right : (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) ≤ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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)
⊢ a ≤ (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ)
have nlinarith : (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) < a →
  (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) - a + (0 - (a - (↑x : ℝ)) * ((↑t : ℝ) - 1)) +
      (0 - (a - (↑y : ℝ)) * (0 - (↑t : ℝ))) =
    0
Tactic: nlinarith [x.2.1, y.2.1, t.2.1, t.2.2]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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)
⊢ (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) ≤ b
have nlinarith : b < (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) →
  b - ((1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ)) + (0 - ((↑x : ℝ) - b) * ((↑t : ℝ) - 1)) +
      (0 - ((↑y : ℝ) - b) * (0 - (↑t : ℝ))) =
    0
Tactic: nlinarith [x.2.2, y.2.2, t.2.1, t.2.2]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y : (↑(Icc a b) : Type)
t : (↑unitInterval : Type)
⊢ convexComb x y (unitInterval.symm t) = convexComb y x t
have simp : (↑t : ℝ) * (↑x : ℝ) + (1 - (↑t : ℝ)) * (↑y : ℝ) = (1 - (↑t : ℝ)) * (↑y : ℝ) + (↑t : ℝ) * (↑x : ℝ)
Tactic: simp [convexComb]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y : (↑(Icc a b) : Type)
h : x ≤ y
t : (↑unitInterval : Type)
⊢ x ≤ convexComb x y t
have rw : ∀ (h : (↑x : ℝ) ≤ (↑y : ℝ)) (t : (↑unitInterval : Type)), (↑x : ℝ) ≤ (↑(convexComb x y t) : ℝ)
Tactic: rw [← Subtype.coe_le_coe] at h ⊢
Cleared hypotheses: h, t
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y : (↑(Icc a b) : Type)
h : (↑x : ℝ) ≤ (↑y : ℝ)
t : (↑unitInterval : Type)
⊢ (↑x : ℝ) ≤ (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ)
have nlinarith : (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) < (↑x : ℝ) →
  (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) - (↑x : ℝ) + (0 - ((↑x : ℝ) - (↑y : ℝ)) * (0 - (↑t : ℝ))) = 0
Tactic: nlinarith [t.2.1, t.2.2]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y : (↑(Icc a b) : Type)
h : x ≤ y
t : (↑unitInterval : Type)
⊢ convexComb x y t ≤ y
have rw : ∀ (h : (↑x : ℝ) ≤ (↑y : ℝ)) (t : (↑unitInterval : Type)), (↑(convexComb x y t) : ℝ) ≤ (↑y : ℝ)
Tactic: rw [← Subtype.coe_le_coe] at h ⊢
Cleared hypotheses: h, t
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
a b : ℝ
x y : (↑(Icc a b) : Type)
h : (↑x : ℝ) ≤ (↑y : ℝ)
t : (↑unitInterval : Type)
⊢ (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) ≤ (↑y : ℝ)
have nlinarith : (↑y : ℝ) < (1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ) →
  (↑y : ℝ) - ((1 - (↑t : ℝ)) * (↑x : ℝ) + (↑t : ℝ) * (↑y : ℝ)) + (0 - ((↑x : ℝ) - (↑y : ℝ)) * ((↑t : ℝ) - 1)) = 0
Tactic: nlinarith [t.2.1, t.2.2]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
α : Type ?u.110642
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
δ : α
s t : (↑unitInterval : Type)
⊢ 0 ≤ (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ))
have ha : 0 ≤ (↑s : ℝ) * (1 - (↑t : ℝ))
Tactic: apply div_nonneg
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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 : ℝ))
⊢ 0 ≤ (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ))
have hb : 0 ≤ 1 - (↑s : ℝ) * (↑t : ℝ)
Tactic: apply div_nonneg
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
α : Type ?u.110642
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
δ : α
s t : (↑unitInterval : Type)
⊢ 0 ≤ (↑s : ℝ) * (1 - (↑t : ℝ))
have nlinarith : (↑s : ℝ) * (1 - (↑t : ℝ)) < 0 → (↑s : ℝ) * (1 - (↑t : ℝ)) - 0 + (0 - (0 - (↑s : ℝ)) * ((↑t : ℝ) - 1)) = 0
Tactic: nlinarith [s.2.1, t.2.2]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
α : Type ?u.110642
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
δ : α
s t : (↑unitInterval : Type)
⊢ 0 ≤ 1 - (↑s : ℝ) * (↑t : ℝ)
have nlinarith : 1 - (↑s : ℝ) * (↑t : ℝ) < 0 → 1 - (↑s : ℝ) * (↑t : ℝ) - 0 + ((↑t : ℝ) - 1) + (0 - ((↑s : ℝ) - 1) * (0 - (↑t : ℝ))) = 0
Tactic: nlinarith [s.2.2, t.2.2, t.2.1]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
α : Type ?u.110642
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
δ : α
s t : (↑unitInterval : Type)
⊢ (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ)) ≤ 1
have h₁ : (↑s : ℝ) * (1 - (↑t : ℝ)) ≤ 1 - (↑s : ℝ) * (↑t : ℝ)
Tactic: apply div_le_one_of_le₀
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
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 : ℝ)
⊢ (↑s : ℝ) * (1 - (↑t : ℝ)) / (1 - (↑s : ℝ) * (↑t : ℝ)) ≤ 1
have hb : 0 ≤ 1 - (↑s : ℝ) * (↑t : ℝ)
Tactic: apply div_le_one_of_le₀
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
α : Type ?u.110642
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
δ : α
s t : (↑unitInterval : Type)
⊢ (↑s : ℝ) * (1 - (↑t : ℝ)) ≤ 1 - (↑s : ℝ) * (↑t : ℝ)
have nlinarith : 1 - (↑s : ℝ) * (↑t : ℝ) < (↑s : ℝ) * (1 - (↑t : ℝ)) →
  1 - (↑s : ℝ) * (↑t : ℝ) - (↑s : ℝ) * (1 - (↑t : ℝ)) + ((↑s : ℝ) - 1) = 0
Tactic: nlinarith [s.2.2]
-- 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 y z t) s =
    convexComb (convexComb x y (convexComb_assoc_coeff₁ s t)) z (convexComb_assoc_coeff₂ s t)
have 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 : ℝ)
Tactic: simp only [convexComb, coe_mul, Subtype.mk.injEq]