awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
linarith : 2 * (↑t : ℝ) < 0 → 2 / 2 = 1
linarith₁ : 2 * (↑t : ℝ) < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2 * (↑t : ℝ) < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ 2 * (↑t : ℝ)
have linarith₃ : 2 * (↑t : ℝ) < 0 → 2 * (↑t : ℝ) - 0 + 2 * (0 - (↑t : ℝ)) = 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
⊢ 2 * (↑t : ℝ) ≤ 1
have linarith : 1 < 2 * (↑t : ℝ) → 2 / 2 = 1
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
linarith : 1 < 2 * (↑t : ℝ) → 2 / 2 = 1
⊢ 2 * (↑t : ℝ) ≤ 1
have linarith₁ : 1 < 2 * (↑t : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
linarith : 1 < 2 * (↑t : ℝ) → 2 / 2 = 1
linarith₁ : 1 < 2 * (↑t : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 2 * (↑t : ℝ) ≤ 1
have linarith₂ : 1 < 2 * (↑t : ℝ) → GT.gt (α := ℝ) 2 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
linarith : 1 < 2 * (↑t : ℝ) → 2 / 2 = 1
linarith₁ : 1 < 2 * (↑t : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 < 2 * (↑t : ℝ) → GT.gt (α := ℝ) 2 0
⊢ 2 * (↑t : ℝ) ≤ 1
have linarith₃ : 1 < 2 * (↑t : ℝ) → 2 * (↑t : ℝ) - HMul.hMul (α := ℝ) 1 1 + (1 - 2 * (↑t : ℝ)) = 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
⊢ LE.le (α := ℝ) 0 1
have linarith : LT.lt (α := ℝ) 1 0 → 2 / 2 = 1
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
linarith : LT.lt (α := ℝ) 1 0 → 2 / 2 = 1
⊢ LE.le (α := ℝ) 0 1
have linarith₁ : LT.lt (α := ℝ) 1 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
linarith : LT.lt (α := ℝ) 1 0 → 2 / 2 = 1
linarith₁ : LT.lt (α := ℝ) 1 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ LE.le (α := ℝ) 0 1
have linarith₂ : LT.lt (α := ℝ) 1 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
linarith : LT.lt (α := ℝ) 1 0 → 2 / 2 = 1
linarith₁ : LT.lt (α := ℝ) 1 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : LT.lt (α := ℝ) 1 0 → GT.gt (α := ℝ) 2 0
⊢ LE.le (α := ℝ) 0 1
have linarith₃ : LT.lt (α := ℝ) 1 0 → -1 + HSub.hSub (α := ℝ) 1 0 = 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
⊢ LE.le (α := ℝ) 1 1
have linarith : LT.lt (α := ℝ) 1 1 → 2 / 2 = 1
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
linarith : LT.lt (α := ℝ) 1 1 → 2 / 2 = 1
⊢ LE.le (α := ℝ) 1 1
have linarith₁ : LT.lt (α := ℝ) 1 1 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
linarith : LT.lt (α := ℝ) 1 1 → 2 / 2 = 1
linarith₁ : LT.lt (α := ℝ) 1 1 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ LE.le (α := ℝ) 1 1
have linarith₂ : LT.lt (α := ℝ) 1 1 → GT.gt (α := ℝ) 2 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
linarith : LT.lt (α := ℝ) 1 1 → 2 / 2 = 1
linarith₁ : LT.lt (α := ℝ) 1 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : LT.lt (α := ℝ) 1 1 → GT.gt (α := ℝ) 2 0
⊢ LE.le (α := ℝ) 1 1
have linarith₃ : LT.lt (α := ℝ) 1 1 → HSub.hSub (α := ℝ) 1 1 = 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
⊢ p.trans (Path.refl x₁) =
    p.reparam (fun (t : (↑I : Type)) ↦ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (transReflReparamAux t) ⋯)
      trans_refl_reparam._proof_1 ⋯ ⋯
have a : ∀ (x : (↑I : Type)),
  Eq (α := X) ((p.trans (Path.refl x₁) : (a : (↑I : Type)) → X) x : X)
    ((p.reparam (fun (t : (↑I : Type)) ↦ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (transReflReparamAux t) sorry)
            trans_refl_reparam._proof_1 sorry sorry :
          (a : (↑I : Type)) → X)
        x :
      X)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x : (↑I : Type)
⊢ Eq (α := X) ((p.trans (Path.refl x₁) : (a : (↑I : Type)) → X) x : X)
    ((p.reparam (fun (t : (↑I : Type)) ↦ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (transReflReparamAux t) ⋯)
            trans_refl_reparam._proof_1 ⋯ ⋯ :
          (a : (↑I : Type)) → X)
        x :
      X)
have a : Eq (α := X) ((p.trans (Path.refl x₁) : (a : (↑I : Type)) → X) x : X)
  ((p.reparam
          (fun (t : (↑I : Type)) ↦
            Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1) sorry)
          trans_refl_reparam._proof_1 sorry sorry :
        (a : (↑I : Type)) → X)
      x :
    X)
Tactic: unfold transReflReparamAux
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x : (↑I : Type)
⊢ Eq (α := X) ((p.trans (Path.refl x₁) : (a : (↑I : Type)) → X) x : X)
    ((p.reparam
            (fun (t : (↑I : Type)) ↦
              Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1) ⋯)
            trans_refl_reparam._proof_1 ⋯ ⋯ :
          (a : (↑I : Type)) → X)
        x :
      X)
have a : Eq (α := X) ((p.trans (Path.refl x₁) : (a : (↑I : Type)) → X) x : X)
  (Function.comp (β := (↑I : Type)) (⇑p : (a : (↑I : Type)) → X)
      (fun (t : (↑I : Type)) ↦ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1) sorry)
      x :
    X)
Tactic: simp only [coe_reparam]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
⊢ (if (↑t : ℝ) ≤ 1 / 4 then 2 * (↑t : ℝ) else if (↑t : ℝ) ≤ 1 / 2 then (↑t : ℝ) + 1 / 4 else 1 / 2 * ((↑t : ℝ) + 1)) ∈ I
have pos : (↑t : ℝ) ≤ 1 / 4 → 2 * (↑t : ℝ) ∈ I
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
pos : (↑t : ℝ) ≤ 1 / 4 → 2 * (↑t : ℝ) ∈ I
⊢ (if (↑t : ℝ) ≤ 1 / 4 then 2 * (↑t : ℝ) else if (↑t : ℝ) ≤ 1 / 2 then (↑t : ℝ) + 1 / 4 else 1 / 2 * ((↑t : ℝ) + 1)) ∈ I
have pos₁ : ¬(↑t : ℝ) ≤ 1 / 4 → (↑t : ℝ) ≤ 1 / 2 → (↑t : ℝ) + 1 / 4 ∈ I
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
pos : (↑t : ℝ) ≤ 1 / 4 → 2 * (↑t : ℝ) ∈ I
pos₁ : ¬(↑t : ℝ) ≤ 1 / 4 → (↑t : ℝ) ≤ 1 / 2 → (↑t : ℝ) + 1 / 4 ∈ I
⊢ (if (↑t : ℝ) ≤ 1 / 4 then 2 * (↑t : ℝ) else if (↑t : ℝ) ≤ 1 / 2 then (↑t : ℝ) + 1 / 4 else 1 / 2 * ((↑t : ℝ) + 1)) ∈ I
have neg : ¬(↑t : ℝ) ≤ 1 / 4 → ¬(↑t : ℝ) ≤ 1 / 2 → 1 / 2 * ((↑t : ℝ) + 1) ∈ I
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 4
⊢ 2 * (↑t : ℝ) ∈ I
have pos : 0 ≤ 2 * (↑t : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 4
pos : 0 ≤ 2 * (↑t : ℝ)
⊢ 2 * (↑t : ℝ) ∈ I
have pos₁ : 2 * (↑t : ℝ) ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
⊢ (↑t : ℝ) + 1 / 4 ∈ I
have pos : 0 ≤ (↑t : ℝ) + 1 / 4
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
pos : 0 ≤ (↑t : ℝ) + 1 / 4
⊢ (↑t : ℝ) + 1 / 4 ∈ I
have pos₁ : (↑t : ℝ) + 1 / 4 ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
⊢ 1 / 2 * ((↑t : ℝ) + 1) ∈ I
have neg : 0 ≤ 1 / 2 * ((↑t : ℝ) + 1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
neg : 0 ≤ 1 / 2 * ((↑t : ℝ) + 1)
⊢ 1 / 2 * ((↑t : ℝ) + 1) ∈ I
have neg₁ : 1 / 2 * ((↑t : ℝ) + 1) ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 4
⊢ 0 ≤ 2 * (↑t : ℝ)
have linarith : 2 * (↑t : ℝ) < 0 → 4 / 4 = 1
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 4
linarith : 2 * (↑t : ℝ) < 0 → 4 / 4 = 1
⊢ 0 ≤ 2 * (↑t : ℝ)
have linarith₁ : 2 * (↑t : ℝ) < 0 → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 4
linarith : 2 * (↑t : ℝ) < 0 → 4 / 4 = 1
linarith₁ : 2 * (↑t : ℝ) < 0 → HMul.hMul (α := ℝ) 1 4 = 4
⊢ 0 ≤ 2 * (↑t : ℝ)
have linarith₂ : 2 * (↑t : ℝ) < 0 → GT.gt (α := ℝ) 4 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 4
linarith : 2 * (↑t : ℝ) < 0 → 4 / 4 = 1
linarith₁ : 2 * (↑t : ℝ) < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 2 * (↑t : ℝ) < 0 → GT.gt (α := ℝ) 4 0
⊢ 0 ≤ 2 * (↑t : ℝ)
have linarith₃ : 2 * (↑t : ℝ) < 0 → 2 * (↑t : ℝ) - 0 + 2 * (0 - (↑t : ℝ)) = 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 4
linarith : 2 * (↑t : ℝ) < 0 → 4 / 4 = 1
linarith₁ : 2 * (↑t : ℝ) < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 2 * (↑t : ℝ) < 0 → GT.gt (α := ℝ) 4 0
linarith₃ : 2 * (↑t : ℝ) < 0 → 2 * (↑t : ℝ) - 0 + 2 * (0 - (↑t : ℝ)) = 0
⊢ 0 ≤ 2 * (↑t : ℝ)
have linarith₄ : 2 * (↑t : ℝ) < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 4
⊢ 2 * (↑t : ℝ) ≤ 1
have linarith : 1 < 2 * (↑t : ℝ) → 4 / 4 = 1
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 4
linarith : 1 < 2 * (↑t : ℝ) → 4 / 4 = 1
⊢ 2 * (↑t : ℝ) ≤ 1
have linarith₁ : 1 < 2 * (↑t : ℝ) → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 4
linarith : 1 < 2 * (↑t : ℝ) → 4 / 4 = 1
linarith₁ : 1 < 2 * (↑t : ℝ) → HMul.hMul (α := ℝ) 1 4 = 4
⊢ 2 * (↑t : ℝ) ≤ 1
have linarith₂ : 1 < 2 * (↑t : ℝ) → GT.gt (α := ℝ) 4 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 4
linarith : 1 < 2 * (↑t : ℝ) → 4 / 4 = 1
linarith₁ : 1 < 2 * (↑t : ℝ) → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 1 < 2 * (↑t : ℝ) → GT.gt (α := ℝ) 4 0
⊢ 2 * (↑t : ℝ) ≤ 1
have linarith₃ : 1 < 2 * (↑t : ℝ) → -1 + (4 * (↑t : ℝ) - HMul.hMul (α := ℝ) 1 1) + 2 * (1 - 2 * (↑t : ℝ)) = 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 4
linarith : 1 < 2 * (↑t : ℝ) → 4 / 4 = 1
linarith₁ : 1 < 2 * (↑t : ℝ) → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 1 < 2 * (↑t : ℝ) → GT.gt (α := ℝ) 4 0
linarith₃ : 1 < 2 * (↑t : ℝ) → -1 + (4 * (↑t : ℝ) - HMul.hMul (α := ℝ) 1 1) + 2 * (1 - 2 * (↑t : ℝ)) = 0
⊢ 2 * (↑t : ℝ) ≤ 1
have linarith₄ : 1 < 2 * (↑t : ℝ) → GT.gt (α := ℝ) 2 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
⊢ 0 ≤ (↑t : ℝ) + 1 / 4
have linarith : (↑t : ℝ) + 1 / 4 < 0 → 4 / 4 = 1
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
linarith : (↑t : ℝ) + 1 / 4 < 0 → 4 / 4 = 1
⊢ 0 ≤ (↑t : ℝ) + 1 / 4
have linarith₁ : (↑t : ℝ) + 1 / 4 < 0 → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
linarith : (↑t : ℝ) + 1 / 4 < 0 → 4 / 4 = 1
linarith₁ : (↑t : ℝ) + 1 / 4 < 0 → HMul.hMul (α := ℝ) 1 4 = 4
⊢ 0 ≤ (↑t : ℝ) + 1 / 4
have linarith₂ : (↑t : ℝ) + 1 / 4 < 0 → GT.gt (α := ℝ) 4 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
linarith : (↑t : ℝ) + 1 / 4 < 0 → 4 / 4 = 1
linarith₁ : (↑t : ℝ) + 1 / 4 < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : (↑t : ℝ) + 1 / 4 < 0 → GT.gt (α := ℝ) 4 0
⊢ 0 ≤ (↑t : ℝ) + 1 / 4
have linarith₃ : (↑t : ℝ) + 1 / 4 < 0 → 2 / 2 = 1
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
linarith : (↑t : ℝ) + 1 / 4 < 0 → 4 / 4 = 1
linarith₁ : (↑t : ℝ) + 1 / 4 < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : (↑t : ℝ) + 1 / 4 < 0 → GT.gt (α := ℝ) 4 0
linarith₃ : (↑t : ℝ) + 1 / 4 < 0 → 2 / 2 = 1
⊢ 0 ≤ (↑t : ℝ) + 1 / 4
have linarith₄ : (↑t : ℝ) + 1 / 4 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
linarith : (↑t : ℝ) + 1 / 4 < 0 → 4 / 4 = 1
linarith₁ : (↑t : ℝ) + 1 / 4 < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : (↑t : ℝ) + 1 / 4 < 0 → GT.gt (α := ℝ) 4 0
linarith₃ : (↑t : ℝ) + 1 / 4 < 0 → 2 / 2 = 1
linarith₄ : (↑t : ℝ) + 1 / 4 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 ≤ (↑t : ℝ) + 1 / 4
have linarith₅ : (↑t : ℝ) + 1 / 4 < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
linarith : (↑t : ℝ) + 1 / 4 < 0 → 4 / 4 = 1
linarith₁ : (↑t : ℝ) + 1 / 4 < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : (↑t : ℝ) + 1 / 4 < 0 → GT.gt (α := ℝ) 4 0
linarith₃ : (↑t : ℝ) + 1 / 4 < 0 → 2 / 2 = 1
linarith₄ : (↑t : ℝ) + 1 / 4 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : (↑t : ℝ) + 1 / 4 < 0 → GT.gt (α := ℝ) 2 0
linarith₆ : (↑t : ℝ) + 1 / 4 < 0 → 4 / 4 = 1
linarith₇ : (↑t : ℝ) + 1 / 4 < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₈ : (↑t : ℝ) + 1 / 4 < 0 → GT.gt (α := ℝ) 4 0
⊢ 0 ≤ (↑t : ℝ) + 1 / 4
have linarith₉ : (↑t : ℝ) + 1 / 4 < 0 →
  HMul.hMul (α := ℝ) 2 (-1) + (HMul.hMul (α := ℝ) 1 1 - 4 * (↑t : ℝ)) +
      (4 * (↑t : ℝ) + HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 4 0) =
    0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
⊢ (↑t : ℝ) + 1 / 4 ≤ 1
have linarith : 1 < (↑t : ℝ) + 1 / 4 → 4 / 4 = 1
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
linarith : 1 < (↑t : ℝ) + 1 / 4 → 4 / 4 = 1
⊢ (↑t : ℝ) + 1 / 4 ≤ 1
have linarith₁ : 1 < (↑t : ℝ) + 1 / 4 → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
linarith : 1 < (↑t : ℝ) + 1 / 4 → 4 / 4 = 1
linarith₁ : 1 < (↑t : ℝ) + 1 / 4 → HMul.hMul (α := ℝ) 1 4 = 4
⊢ (↑t : ℝ) + 1 / 4 ≤ 1
have linarith₂ : 1 < (↑t : ℝ) + 1 / 4 → GT.gt (α := ℝ) 4 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
linarith : 1 < (↑t : ℝ) + 1 / 4 → 4 / 4 = 1
linarith₁ : 1 < (↑t : ℝ) + 1 / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 1 < (↑t : ℝ) + 1 / 4 → GT.gt (α := ℝ) 4 0
⊢ (↑t : ℝ) + 1 / 4 ≤ 1
have linarith₃ : 1 < (↑t : ℝ) + 1 / 4 → 2 / 2 = 1
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
linarith : 1 < (↑t : ℝ) + 1 / 4 → 4 / 4 = 1
linarith₁ : 1 < (↑t : ℝ) + 1 / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 1 < (↑t : ℝ) + 1 / 4 → GT.gt (α := ℝ) 4 0
linarith₃ : 1 < (↑t : ℝ) + 1 / 4 → 2 / 2 = 1
⊢ (↑t : ℝ) + 1 / 4 ≤ 1
have linarith₄ : 1 < (↑t : ℝ) + 1 / 4 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
linarith : 1 < (↑t : ℝ) + 1 / 4 → 4 / 4 = 1
linarith₁ : 1 < (↑t : ℝ) + 1 / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 1 < (↑t : ℝ) + 1 / 4 → GT.gt (α := ℝ) 4 0
linarith₃ : 1 < (↑t : ℝ) + 1 / 4 → 2 / 2 = 1
linarith₄ : 1 < (↑t : ℝ) + 1 / 4 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ (↑t : ℝ) + 1 / 4 ≤ 1
have linarith₅ : 1 < (↑t : ℝ) + 1 / 4 → GT.gt (α := ℝ) 2 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
linarith : 1 < (↑t : ℝ) + 1 / 4 → 4 / 4 = 1
linarith₁ : 1 < (↑t : ℝ) + 1 / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 1 < (↑t : ℝ) + 1 / 4 → GT.gt (α := ℝ) 4 0
linarith₃ : 1 < (↑t : ℝ) + 1 / 4 → 2 / 2 = 1
linarith₄ : 1 < (↑t : ℝ) + 1 / 4 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : 1 < (↑t : ℝ) + 1 / 4 → GT.gt (α := ℝ) 2 0
linarith₆ : 1 < (↑t : ℝ) + 1 / 4 → 4 / 4 = 1
linarith₇ : 1 < (↑t : ℝ) + 1 / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₈ : 1 < (↑t : ℝ) + 1 / 4 → GT.gt (α := ℝ) 4 0
⊢ (↑t : ℝ) + 1 / 4 ≤ 1
have linarith₉ : 1 < (↑t : ℝ) + 1 / 4 →
  -1 + 2 * (2 * (↑t : ℝ) - HMul.hMul (α := ℝ) 1 1) +
      (HMul.hMul (α := ℝ) 4 1 - (4 * (↑t : ℝ) + HMul.hMul (α := ℝ) 1 1)) =
    0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
⊢ 0 ≤ 1 / 2 * ((↑t : ℝ) + 1)
have linarith : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 2 / 2 = 1
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 2 / 2 = 1
⊢ 0 ≤ 1 / 2 * ((↑t : ℝ) + 1)
have linarith₁ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 2 / 2 = 1
linarith₁ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 ≤ 1 / 2 * ((↑t : ℝ) + 1)
have linarith₂ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 2 / 2 = 1
linarith₁ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 2 1 = 2
⊢ 0 ≤ 1 / 2 * ((↑t : ℝ) + 1)
have linarith₃ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 2 / 2 = 1
linarith₁ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → GT.gt (α := ℝ) 2 0
linarith₄ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 2 / 2 = 1
linarith₅ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ 1 / 2 * ((↑t : ℝ) + 1)
have linarith₇ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 4 / 4 = 1
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 2 / 2 = 1
linarith₁ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → GT.gt (α := ℝ) 2 0
linarith₄ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 2 / 2 = 1
linarith₅ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → GT.gt (α := ℝ) 2 0
linarith₇ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 4 / 4 = 1
⊢ 0 ≤ 1 / 2 * ((↑t : ℝ) + 1)
have linarith₈ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 2 / 2 = 1
linarith₁ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → GT.gt (α := ℝ) 2 0
linarith₄ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 2 / 2 = 1
linarith₅ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → GT.gt (α := ℝ) 2 0
linarith₇ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 4 / 4 = 1
linarith₈ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 1 4 = 4
⊢ 0 ≤ 1 / 2 * ((↑t : ℝ) + 1)
have linarith₉ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → GT.gt (α := ℝ) 4 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]