awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
ι : Type u_3
χ : ι → Type u_4
inst : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : (↑I : Type)
i : ι
⊢ Eq.{u_4 + 1} (α := χ i)
    (((Path.pi (χ := χ) γ₀).trans (Path.pi (χ := χ) γ₁) : (a : (↑I : Type)) → (i : ι) → χ i) t i : χ i)
    ((Path.pi (χ := χ) fun (i : ι) ↦ (γ₀ i).trans (γ₁ i) : (a : (↑I : Type)) → (i : ι) → χ i) t i : χ i)
have a : Eq.{u_4 + 1} (α := χ i)
  (({
          toFun :=
            (fun (t : ℝ) ↦
                if t ≤ 1 / 2 then ((Path.pi (χ := χ) γ₀).extend : (a : ℝ) → (i : ι) → χ i) (2 * t)
                else ((Path.pi (χ := χ) γ₁).extend : (a : ℝ) → (i : ι) → χ i) (2 * t - 1)) ∘
              Subtype.val (p := fun (x : ℝ) ↦ x ∈ I),
          continuous_toFun := sorry, source' := sorry, target' := sorry : Path as cs } :
        (a : (↑I : Type)) → (i : ι) → χ i)
      t i :
    χ i)
  ((Path.pi (χ := χ) fun (i : ι) ↦
          {
            toFun :=
              (fun (t : ℝ) ↦
                  if t ≤ 1 / 2 then ((γ₀ i).extend : (a : ℝ) → χ i) (2 * t)
                  else ((γ₁ i).extend : (a : ℝ) → χ i) (2 * t - 1)) ∘
                Subtype.val (p := fun (x : ℝ) ↦ x ∈ I),
            continuous_toFun := sorry, source' := sorry, target' := sorry } :
        (a : (↑I : Type)) → (i : ι) → χ i)
      t i :
    χ i)
Tactic: unfold Path.trans
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
ι : Type u_3
χ : ι → Type u_4
inst : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : (↑I : Type)
i : ι
⊢ Eq.{u_4 + 1} (α := χ i)
    (({
            toFun :=
              (fun (t : ℝ) ↦
                  if t ≤ 1 / 2 then ((Path.pi (χ := χ) γ₀).extend : (a : ℝ) → (i : ι) → χ i) (2 * t)
                  else ((Path.pi (χ := χ) γ₁).extend : (a : ℝ) → (i : ι) → χ i) (2 * t - 1)) ∘
                Subtype.val (p := fun (x : ℝ) ↦ x ∈ I),
            continuous_toFun := ⋯, source' := ⋯, target' := ⋯ : Path as cs } :
          (a : (↑I : Type)) → (i : ι) → χ i)
        t i :
      χ i)
    ((Path.pi (χ := χ) fun (i : ι) ↦
            {
              toFun :=
                (fun (t : ℝ) ↦
                    if t ≤ 1 / 2 then ((γ₀ i).extend : (a : ℝ) → χ i) (2 * t)
                    else ((γ₁ i).extend : (a : ℝ) → χ i) (2 * t - 1)) ∘
                  Subtype.val (p := fun (x : ℝ) ↦ x ∈ I),
              continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } :
          (a : (↑I : Type)) → (i : ι) → χ i)
        t i :
      χ i)
have a : Eq.{u_4 + 1} (α := χ i)
  ((if (↑t : ℝ) ≤ 1 / 2 then ((Path.pi (χ := χ) γ₀).extend : (a : ℝ) → (i : ι) → χ i) (2 * (↑t : ℝ))
      else ((Path.pi (χ := χ) γ₁).extend : (a : ℝ) → (i : ι) → χ i) (2 * (↑t : ℝ) - 1))
      i :
    χ i)
  (if (↑t : ℝ) ≤ 1 / 2 then ((γ₀ i).extend : (a : ℝ) → χ i) (2 * (↑t : ℝ))
    else ((γ₁ i).extend : (a : ℝ) → χ i) (2 * (↑t : ℝ) - 1) :
    χ i)
Tactic: simp only [Path.coe_mk_mk, Function.comp_apply, pi_coe]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
ι : Type u_3
χ : ι → Type u_4
inst : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : (↑I : Type)
i : ι
⊢ Eq.{u_4 + 1} (α := χ i)
    ((if (↑t : ℝ) ≤ 1 / 2 then ((Path.pi (χ := χ) γ₀).extend : (a : ℝ) → (i : ι) → χ i) (2 * (↑t : ℝ))
        else ((Path.pi (χ := χ) γ₁).extend : (a : ℝ) → (i : ι) → χ i) (2 * (↑t : ℝ) - 1))
        i :
      χ i)
    (if (↑t : ℝ) ≤ 1 / 2 then ((γ₀ i).extend : (a : ℝ) → χ i) (2 * (↑t : ℝ))
      else ((γ₁ i).extend : (a : ℝ) → χ i) (2 * (↑t : ℝ) - 1) :
      χ i)
have pos : (↑t : ℝ) ≤ 1 / 2 →
  Eq.{u_4 + 1} (α := χ i) (((Path.pi (χ := χ) γ₀).extend : (a : ℝ) → (i : ι) → χ i) (2 * (↑t : ℝ)) i : χ i)
    (((γ₀ i).extend : (a : ℝ) → χ i) (2 * (↑t : ℝ)) : χ i)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
ι : Type u_3
χ : ι → Type u_4
inst : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : (↑I : Type)
i : ι
pos :
  (↑t : ℝ) ≤ 1 / 2 →
    Eq.{u_4 + 1} (α := χ i) (((Path.pi (χ := χ) γ₀).extend : (a : ℝ) → (i : ι) → χ i) (2 * (↑t : ℝ)) i : χ i)
      (((γ₀ i).extend : (a : ℝ) → χ i) (2 * (↑t : ℝ)) : χ i)
⊢ Eq.{u_4 + 1} (α := χ i)
    ((if (↑t : ℝ) ≤ 1 / 2 then ((Path.pi (χ := χ) γ₀).extend : (a : ℝ) → (i : ι) → χ i) (2 * (↑t : ℝ))
        else ((Path.pi (χ := χ) γ₁).extend : (a : ℝ) → (i : ι) → χ i) (2 * (↑t : ℝ) - 1))
        i :
      χ i)
    (if (↑t : ℝ) ≤ 1 / 2 then ((γ₀ i).extend : (a : ℝ) → χ i) (2 * (↑t : ℝ))
      else ((γ₁ i).extend : (a : ℝ) → χ i) (2 * (↑t : ℝ) - 1) :
      χ i)
have neg : ¬(↑t : ℝ) ≤ 1 / 2 →
  Eq.{u_4 + 1} (α := χ i) (((Path.pi (χ := χ) γ₁).extend : (a : ℝ) → (i : ι) → χ i) (2 * (↑t : ℝ) - 1) i : χ i)
    (((γ₁ i).extend : (a : ℝ) → χ i) (2 * (↑t : ℝ) - 1) : χ i)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
γ_1 : Path x y
X : Type u_4
inst_2 : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) (min (max (↑0 : ℝ) t₀) t₁) : X) ((γ.extend : (a : ℝ) → X) (min t₀ t₁) : X)
have simp : Eq (α := X)
  ((γ.extend : (a : ℝ) → X)
      (if (if t₀ ≤ (↑0 : ℝ) then (↑0 : ℝ) else t₀) ≤ t₁ then if t₀ ≤ (↑0 : ℝ) then (↑0 : ℝ) else t₀ else t₁) :
    X)
  ((γ.extend : (a : ℝ) → X) (if t₀ ≤ t₁ then t₀ else t₁) : X)
Tactic: simp only [min_def, max_def']
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
γ_1 : Path x y
X : Type u_4
inst_2 : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ Eq (α := X)
    ((γ.extend : (a : ℝ) → X)
        (if (if t₀ ≤ (↑0 : ℝ) then (↑0 : ℝ) else t₀) ≤ t₁ then if t₀ ≤ (↑0 : ℝ) then (↑0 : ℝ) else t₀ else t₁) :
      X)
    ((γ.extend : (a : ℝ) → X) (if t₀ ≤ t₁ then t₀ else t₁) : X)
have pos : ∀ (h₁ : t₀ ≤ (↑0 : ℝ)) (h₂ : (↑0 : ℝ) ≤ t₁) (h₃ : t₀ ≤ t₁),
  Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑0 : ℝ) : X) ((γ.extend : (a : ℝ) → X) t₀ : X)
Tactic: split_ifs with h₁ h₂ h₃ h₄
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
γ_1 : Path x y
X : Type u_4
inst_2 : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
pos :
  ∀ (h₁ : t₀ ≤ (↑0 : ℝ)) (h₂ : (↑0 : ℝ) ≤ t₁) (h₃ : t₀ ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑0 : ℝ) : X) ((γ.extend : (a : ℝ) → X) t₀ : X)
⊢ Eq (α := X)
    ((γ.extend : (a : ℝ) → X)
        (if (if t₀ ≤ (↑0 : ℝ) then (↑0 : ℝ) else t₀) ≤ t₁ then if t₀ ≤ (↑0 : ℝ) then (↑0 : ℝ) else t₀ else t₁) :
      X)
    ((γ.extend : (a : ℝ) → X) (if t₀ ≤ t₁ then t₀ else t₁) : X)
have neg : ∀ (h₁ : t₀ ≤ (↑0 : ℝ)) (h₂ : (↑0 : ℝ) ≤ t₁) (h₃ : ¬t₀ ≤ t₁),
  Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑0 : ℝ) : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
Tactic: split_ifs with h₁ h₂ h₃ h₄
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
γ_1 : Path x y
X : Type u_4
inst_2 : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
pos :
  ∀ (h₁ : t₀ ≤ (↑0 : ℝ)) (h₂ : (↑0 : ℝ) ≤ t₁) (h₃ : t₀ ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑0 : ℝ) : X) ((γ.extend : (a : ℝ) → X) t₀ : X)
neg :
  ∀ (h₁ : t₀ ≤ (↑0 : ℝ)) (h₂ : (↑0 : ℝ) ≤ t₁) (h₃ : ¬t₀ ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑0 : ℝ) : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
⊢ Eq (α := X)
    ((γ.extend : (a : ℝ) → X)
        (if (if t₀ ≤ (↑0 : ℝ) then (↑0 : ℝ) else t₀) ≤ t₁ then if t₀ ≤ (↑0 : ℝ) then (↑0 : ℝ) else t₀ else t₁) :
      X)
    ((γ.extend : (a : ℝ) → X) (if t₀ ≤ t₁ then t₀ else t₁) : X)
have pos₁ : ∀ (h₁ : t₀ ≤ (↑0 : ℝ)) (h₂ : ¬(↑0 : ℝ) ≤ t₁) (h₄ : t₀ ≤ t₁),
  Eq (α := X) ((γ.extend : (a : ℝ) → X) t₁ : X) ((γ.extend : (a : ℝ) → X) t₀ : X)
Tactic: split_ifs with h₁ h₂ h₃ h₄
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
γ_1 : Path x y
X : Type u_4
inst_2 : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
pos :
  ∀ (h₁ : t₀ ≤ (↑0 : ℝ)) (h₂ : (↑0 : ℝ) ≤ t₁) (h₃ : t₀ ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑0 : ℝ) : X) ((γ.extend : (a : ℝ) → X) t₀ : X)
neg :
  ∀ (h₁ : t₀ ≤ (↑0 : ℝ)) (h₂ : (↑0 : ℝ) ≤ t₁) (h₃ : ¬t₀ ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑0 : ℝ) : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
pos₁ :
  ∀ (h₁ : t₀ ≤ (↑0 : ℝ)) (h₂ : ¬(↑0 : ℝ) ≤ t₁) (h₄ : t₀ ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) t₁ : X) ((γ.extend : (a : ℝ) → X) t₀ : X)
⊢ Eq (α := X)
    ((γ.extend : (a : ℝ) → X)
        (if (if t₀ ≤ (↑0 : ℝ) then (↑0 : ℝ) else t₀) ≤ t₁ then if t₀ ≤ (↑0 : ℝ) then (↑0 : ℝ) else t₀ else t₁) :
      X)
    ((γ.extend : (a : ℝ) → X) (if t₀ ≤ t₁ then t₀ else t₁) : X)
have neg₁ : ∀ (h₁ : t₀ ≤ (↑0 : ℝ)) (h₂ : ¬(↑0 : ℝ) ≤ t₁) (h₄ : ¬t₀ ≤ t₁),
  Eq (α := X) ((γ.extend : (a : ℝ) → X) t₁ : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
Tactic: split_ifs with h₁ h₂ h₃ h₄
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
γ_1 : Path x y
X : Type u_4
inst_2 : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
pos :
  ∀ (h₁ : t₀ ≤ (↑0 : ℝ)) (h₂ : (↑0 : ℝ) ≤ t₁) (h₃ : t₀ ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑0 : ℝ) : X) ((γ.extend : (a : ℝ) → X) t₀ : X)
neg :
  ∀ (h₁ : t₀ ≤ (↑0 : ℝ)) (h₂ : (↑0 : ℝ) ≤ t₁) (h₃ : ¬t₀ ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑0 : ℝ) : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
pos₁ :
  ∀ (h₁ : t₀ ≤ (↑0 : ℝ)) (h₂ : ¬(↑0 : ℝ) ≤ t₁) (h₄ : t₀ ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) t₁ : X) ((γ.extend : (a : ℝ) → X) t₀ : X)
neg₁ :
  ∀ (h₁ : t₀ ≤ (↑0 : ℝ)) (h₂ : ¬(↑0 : ℝ) ≤ t₁) (h₄ : ¬t₀ ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) t₁ : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
⊢ Eq (α := X)
    ((γ.extend : (a : ℝ) → X)
        (if (if t₀ ≤ (↑0 : ℝ) then (↑0 : ℝ) else t₀) ≤ t₁ then if t₀ ≤ (↑0 : ℝ) then (↑0 : ℝ) else t₀ else t₁) :
      X)
    ((γ.extend : (a : ℝ) → X) (if t₀ ≤ t₁ then t₀ else t₁) : X)
have pos₂ : ∀ (h₁ : ¬t₀ ≤ (↑0 : ℝ)), t₀ ≤ t₁ → Eq (α := X) ((γ.extend : (a : ℝ) → X) t₀ : X) ((γ.extend : (a : ℝ) → X) t₀ : X)
Tactic: split_ifs with h₁ h₂ h₃ h₄
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
γ_1 : Path x y
X : Type u_4
inst_2 : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
pos :
  ∀ (h₁ : t₀ ≤ (↑0 : ℝ)) (h₂ : (↑0 : ℝ) ≤ t₁) (h₃ : t₀ ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑0 : ℝ) : X) ((γ.extend : (a : ℝ) → X) t₀ : X)
neg :
  ∀ (h₁ : t₀ ≤ (↑0 : ℝ)) (h₂ : (↑0 : ℝ) ≤ t₁) (h₃ : ¬t₀ ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑0 : ℝ) : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
pos₁ :
  ∀ (h₁ : t₀ ≤ (↑0 : ℝ)) (h₂ : ¬(↑0 : ℝ) ≤ t₁) (h₄ : t₀ ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) t₁ : X) ((γ.extend : (a : ℝ) → X) t₀ : X)
neg₁ :
  ∀ (h₁ : t₀ ≤ (↑0 : ℝ)) (h₂ : ¬(↑0 : ℝ) ≤ t₁) (h₄ : ¬t₀ ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) t₁ : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
pos₂ :
  ∀ (h₁ : ¬t₀ ≤ (↑0 : ℝ)), t₀ ≤ t₁ → Eq (α := X) ((γ.extend : (a : ℝ) → X) t₀ : X) ((γ.extend : (a : ℝ) → X) t₀ : X)
⊢ Eq (α := X)
    ((γ.extend : (a : ℝ) → X)
        (if (if t₀ ≤ (↑0 : ℝ) then (↑0 : ℝ) else t₀) ≤ t₁ then if t₀ ≤ (↑0 : ℝ) then (↑0 : ℝ) else t₀ else t₁) :
      X)
    ((γ.extend : (a : ℝ) → X) (if t₀ ≤ t₁ then t₀ else t₁) : X)
have neg₂ : ∀ (h₁ : ¬t₀ ≤ (↑0 : ℝ)), ¬t₀ ≤ t₁ → Eq (α := X) ((γ.extend : (a : ℝ) → X) t₁ : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
Tactic: split_ifs with h₁ h₂ h₃ h₄
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
γ_1 : Path x y
X : Type u_4
inst_2 : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : t₀ ≤ (↑0 : ℝ)
h₂ : (↑0 : ℝ) ≤ t₁
h₃ : ¬t₀ ≤ t₁
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑0 : ℝ) : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
have neg : (↑0 : ℝ) = t₁
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
γ_1 : Path x y
X : Type u_4
inst_2 : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : t₀ ≤ (↑0 : ℝ)
h₂ : (↑0 : ℝ) ≤ t₁
h₃ : ¬t₀ ≤ t₁
⊢ (↑0 : ℝ) = t₁
have linarith : (↑0 : ℝ) < t₁ → t₀ - (↑0 : ℝ) + ((↑0 : ℝ) - t₁) + (t₁ - t₀) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
γ_1 : Path x y
X : Type u_4
inst_2 : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : t₀ ≤ (↑0 : ℝ)
h₂ : (↑0 : ℝ) ≤ t₁
h₃ : ¬t₀ ≤ t₁
linarith : (↑0 : ℝ) < t₁ → t₀ - (↑0 : ℝ) + ((↑0 : ℝ) - t₁) + (t₁ - t₀) = 0
⊢ (↑0 : ℝ) = t₁
have linarith₁ : t₁ < (↑0 : ℝ) → t₀ - (↑0 : ℝ) + ((↑0 : ℝ) - t₁) + (t₁ - t₀) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (hypothesis)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
γ_1 : Path x y
X : Type u_4
inst_2 : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : t₀ ≤ (↑0 : ℝ)
h₂ : ¬(↑0 : ℝ) ≤ t₁
h₄ : t₀ ≤ t₁
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) t₁ : X) ((γ.extend : (a : ℝ) → X) t₀ : X)
have h₅ : t₁ ≤ 0
Tactic: have h₄ : t₁ ≤ 0 := le_of_lt (by simpa using h₂)
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
γ_1 : Path x y
X : Type u_4
inst_2 : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) (min (max (↑1 : ℝ) t₀) t₁) : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
have simp : Eq (α := X)
  ((γ.extend : (a : ℝ) → X)
      (if (if t₀ ≤ (↑1 : ℝ) then (↑1 : ℝ) else t₀) ≤ t₁ then if t₀ ≤ (↑1 : ℝ) then (↑1 : ℝ) else t₀ else t₁) :
    X)
  ((γ.extend : (a : ℝ) → X) t₁ : X)
Tactic: simp only [min_def, max_def']
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
γ_1 : Path x y
X : Type u_4
inst_2 : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ Eq (α := X)
    ((γ.extend : (a : ℝ) → X)
        (if (if t₀ ≤ (↑1 : ℝ) then (↑1 : ℝ) else t₀) ≤ t₁ then if t₀ ≤ (↑1 : ℝ) then (↑1 : ℝ) else t₀ else t₁) :
      X)
    ((γ.extend : (a : ℝ) → X) t₁ : X)
have pos : ∀ (h₁ : t₀ ≤ (↑1 : ℝ)) (h₂ : (↑1 : ℝ) ≤ t₁),
  Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑1 : ℝ) : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
Tactic: split_ifs with h₁ h₂ h₃
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
γ_1 : Path x y
X : Type u_4
inst_2 : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
pos :
  ∀ (h₁ : t₀ ≤ (↑1 : ℝ)) (h₂ : (↑1 : ℝ) ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑1 : ℝ) : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
⊢ Eq (α := X)
    ((γ.extend : (a : ℝ) → X)
        (if (if t₀ ≤ (↑1 : ℝ) then (↑1 : ℝ) else t₀) ≤ t₁ then if t₀ ≤ (↑1 : ℝ) then (↑1 : ℝ) else t₀ else t₁) :
      X)
    ((γ.extend : (a : ℝ) → X) t₁ : X)
have neg : ∀ (h₁ : t₀ ≤ (↑1 : ℝ)) (h₂ : ¬(↑1 : ℝ) ≤ t₁),
  Eq (α := X) ((γ.extend : (a : ℝ) → X) t₁ : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
Tactic: split_ifs with h₁ h₂ h₃
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
γ_1 : Path x y
X : Type u_4
inst_2 : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
pos :
  ∀ (h₁ : t₀ ≤ (↑1 : ℝ)) (h₂ : (↑1 : ℝ) ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑1 : ℝ) : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
neg :
  ∀ (h₁ : t₀ ≤ (↑1 : ℝ)) (h₂ : ¬(↑1 : ℝ) ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) t₁ : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
⊢ Eq (α := X)
    ((γ.extend : (a : ℝ) → X)
        (if (if t₀ ≤ (↑1 : ℝ) then (↑1 : ℝ) else t₀) ≤ t₁ then if t₀ ≤ (↑1 : ℝ) then (↑1 : ℝ) else t₀ else t₁) :
      X)
    ((γ.extend : (a : ℝ) → X) t₁ : X)
have pos₁ : ∀ (h₁ : ¬t₀ ≤ (↑1 : ℝ)) (h₃ : t₀ ≤ t₁), Eq (α := X) ((γ.extend : (a : ℝ) → X) t₀ : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
Tactic: split_ifs with h₁ h₂ h₃
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
γ_1 : Path x y
X : Type u_4
inst_2 : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
pos :
  ∀ (h₁ : t₀ ≤ (↑1 : ℝ)) (h₂ : (↑1 : ℝ) ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑1 : ℝ) : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
neg :
  ∀ (h₁ : t₀ ≤ (↑1 : ℝ)) (h₂ : ¬(↑1 : ℝ) ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) t₁ : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
pos₁ :
  ∀ (h₁ : ¬t₀ ≤ (↑1 : ℝ)) (h₃ : t₀ ≤ t₁),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) t₀ : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
⊢ Eq (α := X)
    ((γ.extend : (a : ℝ) → X)
        (if (if t₀ ≤ (↑1 : ℝ) then (↑1 : ℝ) else t₀) ≤ t₁ then if t₀ ≤ (↑1 : ℝ) then (↑1 : ℝ) else t₀ else t₁) :
      X)
    ((γ.extend : (a : ℝ) → X) t₁ : X)
have neg₁ : ∀ (h₁ : ¬t₀ ≤ (↑1 : ℝ)) (h₃ : ¬t₀ ≤ t₁), Eq (α := X) ((γ.extend : (a : ℝ) → X) t₁ : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
Tactic: split_ifs with h₁ h₂ h₃
-- Lean 4 proof step from Mathlib.Topology.Path (hypothesis)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
γ_1 : Path x y
X : Type u_4
inst_2 : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ (↑1 : ℝ)
h₃ : t₀ ≤ t₁
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) t₀ : X) ((γ.extend : (a : ℝ) → X) t₁ : X)
have h₄ : 1 ≤ t₀
Tactic: have h₄ : 1 ≤ t₀ := le_of_lt (by simpa using h₁)
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
γ_1 : Path x y
X : Type u_4
inst_2 : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h : t₀ ≤ t₁
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) t₀ : X) ((γ.extend : (a : ℝ) → X) (min t₀ t₁) : X)
have rw : Eq (α := X) ((γ.extend : (a : ℝ) → X) t₀ : X) ((γ.extend : (a : ℝ) → X) t₀ : X)
Tactic: rw [min_eq_left h]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ Subset (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.truncate t₀ t₁) : (a : (↑I : Type)) → X))
    (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
have rw : Subset (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.truncate t₀ t₁) : (a : (↑I : Type)) → X))
  (range (ι := ℝ) (⇑γ.extend : (a : ℝ) → X))
Tactic: rw [← γ.extend_range]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ Subset (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.truncate t₀ t₁) : (a : (↑I : Type)) → X))
    (range (ι := ℝ) (⇑γ.extend : (a : ℝ) → X))
have simp : ∀ (x : ℝ) (h : x ∈ I),
  Membership.mem (α := X) (γ := Set X) (range (ι := ℝ) (⇑γ.extend : (a : ℝ) → X))
    ((γ.truncate t₀ t₁ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) x h) : X)
Tactic: simp only [range_subset_iff, SetCoe.forall]
-- Lean 4 proof step from Mathlib.Topology.Path (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
⊢ Continuous[_, inst] ↿(γ.truncate t)
have key : Continuous (Y := ℝ × ℝ × (↑I : Type)) fun (x : ℝ × (↑I : Type)) ↦ (t, x)
Tactic: have key : Continuous (fun x => (t, x) : ℝ × I → ℝ × ℝ × I) := by fun_prop
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
γ_1 : Path x y
a b : X
γ : Path a b
t : ℝ
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) (min t t) : X) ((γ.extend : (a : ℝ) → X) t : X)
have rw : Eq (α := X) ((γ.extend : (a : ℝ) → X) t : X) ((γ.extend : (a : ℝ) → X) t : X)
Tactic: rw [min_self]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
⊢ γ.truncate t t = cast (refl ((γ.extend : (a : ℝ) → X) t)) ⋯ ⋯
have a₁ : ∀ (x : (↑I : Type)),
  Eq (α := X) ((γ.truncate t t : (a : (↑I : Type)) → X) x : X)
    (((cast (refl ((γ.extend : (a : ℝ) → X) t)) sorry sorry :
            Path (X := X) ((γ.extend : (a : ℝ) → X) (min t t) : X) ((γ.extend : (a : ℝ) → X) t : X)) :
          (a : (↑I : Type)) → X)
        x :
      X)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : (↑I : Type)
⊢ Eq (α := X) ((γ.truncate t t : (a : (↑I : Type)) → X) x : X)
    (((cast (refl ((γ.extend : (a : ℝ) → X) t)) ⋯ ⋯ :
            Path (X := X) ((γ.extend : (a : ℝ) → X) (min t t) : X) ((γ.extend : (a : ℝ) → X) t : X)) :
          (a : (↑I : Type)) → X)
        x :
      X)
have pos : ∀ (hx : (↑x : ℝ) ≤ t),
  Eq (α := X) ((γ.truncate t t : (a : (↑I : Type)) → X) x : X)
    (((cast (refl ((γ.extend : (a : ℝ) → X) t)) sorry sorry :
            Path (X := X) ((γ.extend : (a : ℝ) → X) (min t t) : X) ((γ.extend : (a : ℝ) → X) t : X)) :
          (a : (↑I : Type)) → X)
        x :
      X)
Tactic: by_cases hx : x ≤ t
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : (↑I : Type)
pos :
  ∀ (hx : (↑x : ℝ) ≤ t),
    Eq (α := X) ((γ.truncate t t : (a : (↑I : Type)) → X) x : X)
      (((cast (refl ((γ.extend : (a : ℝ) → X) t)) ⋯ ⋯ :
              Path (X := X) ((γ.extend : (a : ℝ) → X) (min t t) : X) ((γ.extend : (a : ℝ) → X) t : X)) :
            (a : (↑I : Type)) → X)
          x :
        X)
⊢ Eq (α := X) ((γ.truncate t t : (a : (↑I : Type)) → X) x : X)
    (((cast (refl ((γ.extend : (a : ℝ) → X) t)) ⋯ ⋯ :
            Path (X := X) ((γ.extend : (a : ℝ) → X) (min t t) : X) ((γ.extend : (a : ℝ) → X) t : X)) :
          (a : (↑I : Type)) → X)
        x :
      X)
have neg : ∀ (hx : ¬(↑x : ℝ) ≤ t),
  Eq (α := X) ((γ.truncate t t : (a : (↑I : Type)) → X) x : X)
    (((cast (refl ((γ.extend : (a : ℝ) → X) t)) sorry sorry :
            Path (X := X) ((γ.extend : (a : ℝ) → X) (min t t) : X) ((γ.extend : (a : ℝ) → X) t : X)) :
          (a : (↑I : Type)) → X)
        x :
      X)
Tactic: by_cases hx : x ≤ t
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
γ_1 : Path x y
a b : X
γ : Path a b
⊢ (γ.extend : (a : ℝ) → X) (min 0 0) = a
have rw : (γ.extend : (a : ℝ) → X) 0 = a
Tactic: rw [min_self, γ.extend_zero]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
γ_1 : Path x y
a b : X
γ : Path a b
rw : (γ.extend : (a : ℝ) → X) 0 = a
⊢ (γ.extend : (a : ℝ) → X) (min 0 0) = a
have rw₁ : a = a
Tactic: rw [min_self, γ.extend_zero]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
γ_1 : Path x y
a b : X
γ : Path a b
⊢ (γ.extend : (a : ℝ) → X) (min 1 1) = b
have rw : (γ.extend : (a : ℝ) → X) 1 = b
Tactic: rw [min_self, γ.extend_one]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
γ_1 : Path x y
a b : X
γ : Path a b
rw : (γ.extend : (a : ℝ) → X) 1 = b
⊢ (γ.extend : (a : ℝ) → X) (min 1 1) = b
have rw₁ : b = b
Tactic: rw [min_self, γ.extend_one]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
⊢ γ.truncate 0 1 = γ.cast ⋯ ⋯
have a₁ : ∀ (x : (↑I : Type)),
  Eq (α := X) ((γ.truncate 0 1 : (a : (↑I : Type)) → X) x : X) ((γ.cast sorry sorry : (a : (↑I : Type)) → X) x : X)
Tactic: ext x