awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Path
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 : ι
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 := ⋯, 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)
⊢ 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)

Tactic:
unfold Path.trans

Premises used: Path.trans
-- Module: Mathlib.Topology.Path
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 : ι
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)
⊢ 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)

Tactic:
simp only [Path.coe_mk_mk, Function.comp_apply, pi_coe]

Premises used: Path.pi_coe, Path.coe_mk_mk, Function.comp_apply
-- Module: Mathlib.Topology.Path
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)
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)
⊢ 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:
split_ifs
-- Module: Mathlib.Topology.Path
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 : ι
h : (↑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:
rfl
-- Module: Mathlib.Topology.Path
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 : ι
h : ¬(↑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:
rfl
-- Module: Mathlib.Topology.Path
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₁ : ℝ
⊢ Continuous (Y := ℝ) fun (s : (↑I : Type)) ↦ min (max (↑s : ℝ) t₀) t₁

Tactic:
fun_prop
-- Module: Mathlib.Topology.Path
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₁ : ℝ
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)
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) (min (max (↑0 : ℝ) t₀) t₁) : X) ((γ.extend : (a : ℝ) → X) (min t₀ t₁) : X)

Tactic:
simp only [min_def, max_def']

Premises used: max_def', min_def
-- Module: Mathlib.Topology.Path
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)
neg₂ :
  ∀ (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)

Tactic:
split_ifs with h₁ h₂ h₃ h₄
-- Module: Mathlib.Topology.Path
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)

Tactic:
simp [γ.extend_of_le_zero h₁]

Premises used: Path.extend_of_le_zero
-- Module: Mathlib.Topology.Path
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₁
neg : (↑0 : ℝ) = t₁
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑0 : ℝ) : X) ((γ.extend : (a : ℝ) → X) t₁ : X)

Tactic:
congr
-- Module: Mathlib.Topology.Path
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
linarith₁ : t₁ < (↑0 : ℝ) → t₀ - (↑0 : ℝ) + ((↑0 : ℝ) - t₁) + (t₁ - t₀) = 0
⊢ (↑0 : ℝ) = t₁

Tactic:
linarith
-- Module: Mathlib.Topology.Path
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₁
⊢ t₁ < 0

Tactic:
simpa using h₂
-- Module: Mathlib.Topology.Path
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₁
⊢ t₁ ≤ 0

Tactic:
have h₄ : t₁ ≤ 0 := le_of_lt (by simpa using h₂)
-- Module: Mathlib.Topology.Path
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₄_1 : t₀ ≤ t₁
h₄ : t₁ ≤ 0
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) t₁ : X) ((γ.extend : (a : ℝ) → X) t₀ : X)

Tactic:
simp [γ.extend_of_le_zero h₄, γ.extend_of_le_zero h₁]

Premises used: Path.extend_of_le_zero
-- Module: Mathlib.Topology.Path
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)

Tactic:
rfl
-- Module: Mathlib.Topology.Path
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 : t₀ ≤ t₁
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) t₀ : X) ((γ.extend : (a : ℝ) → X) t₀ : X)

Tactic:
rfl
-- Module: Mathlib.Topology.Path
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 : ¬t₀ ≤ t₁
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) t₁ : X) ((γ.extend : (a : ℝ) → X) t₁ : X)

Tactic:
rfl
-- Module: Mathlib.Topology.Path
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₁ : ℝ
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)
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) (min (max (↑1 : ℝ) t₀) t₁) : X) ((γ.extend : (a : ℝ) → X) t₁ : X)

Tactic:
simp only [min_def, max_def']

Premises used: max_def', min_def
-- Module: Mathlib.Topology.Path
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)
neg₁ :
  ∀ (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)

Tactic:
split_ifs with h₁ h₂ h₃
-- Module: Mathlib.Topology.Path
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₂ : (↑1 : ℝ) ≤ t₁
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑1 : ℝ) : X) ((γ.extend : (a : ℝ) → X) t₁ : X)

Tactic:
simp [γ.extend_of_one_le h₂]

Premises used: Path.extend_of_one_le
-- Module: Mathlib.Topology.Path
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₂ : ¬(↑1 : ℝ) ≤ t₁
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) t₁ : X) ((γ.extend : (a : ℝ) → X) t₁ : X)

Tactic:
rfl
-- Module: Mathlib.Topology.Path
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₁
⊢ 1 < t₀

Tactic:
simpa using h₁
-- Module: Mathlib.Topology.Path
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₁
⊢ 1 ≤ t₀

Tactic:
have h₄ : 1 ≤ t₀ := le_of_lt (by simpa using h₁)
-- Module: Mathlib.Topology.Path
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₁
h₄ : 1 ≤ t₀
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) t₀ : X) ((γ.extend : (a : ℝ) → X) t₁ : X)

Tactic:
simp [γ.extend_of_one_le h₄, γ.extend_of_one_le (h₄.trans h₃)]

Premises used: Path.extend_of_one_le, LE.le.trans
-- Module: Mathlib.Topology.Path
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)

Tactic:
rfl
-- Module: Mathlib.Topology.Path
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₁
rw rw₁ : Eq (α := X) ((γ.extend : (a : ℝ) → X) t₀ : X) ((γ.extend : (a : ℝ) → X) t₀ : X)
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) t₀ : X) ((γ.extend : (a : ℝ) → X) (min t₀ t₁) : X)

Tactic:
rw [min_eq_left h]

Premises used: min_eq_left
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
rw :
  Subset (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.truncate t₀ t₁) : (a : (↑I : Type)) → X))
    (range (ι := ℝ) (⇑γ.extend : (a : ℝ) → X))
⊢ Subset (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.truncate t₀ t₁) : (a : (↑I : Type)) → X))
    (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))

Tactic:
rw [← γ.extend_range]

Premises used: Path.extend_range
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
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)
⊢ Subset (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.truncate t₀ t₁) : (a : (↑I : Type)) → X))
    (range (ι := ℝ) (⇑γ.extend : (a : ℝ) → X))

Tactic:
simp only [range_subset_iff, SetCoe.forall]

Premises used: Set.range_subset_iff, SetCoe.forall
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ x : ℝ
_hx : 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 _hx) : X)

Tactic:
simp only [DFunLike.coe, Path.truncate, mem_range_self]

Premises used: Set.mem_range_self, Path.truncate, DFunLike.coe
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
⊢ Continuous[_, inst] fun (x : ℝ × ℝ × (↑I : Type)) ↦ (γ.truncate x.1 x.2.1 : (a : (↑I : Type)) → X) x.2.2

Tactic:
γ.continuous_extend.comp
    (((continuous_subtype_val.comp (continuous_snd.comp continuous_snd)).max continuous_fst).min
      (continuous_fst.comp continuous_snd))

Premises used: continuous_subtype_val, Path.continuous_extend, Continuous.comp, continuous_snd, continuous_fst, Continuous.max, Set.IccExtend, Continuous.min
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
⊢ Continuous (Y := ℝ × ℝ × (↑I : Type)) fun (x : ℝ × (↑I : Type)) ↦ (t, x)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
⊢ Continuous (Y := ℝ × ℝ × (↑I : Type)) fun (x : ℝ × (↑I : Type)) ↦ (t, x)

Tactic:
have key : Continuous (fun x => (t, x) : ℝ × I → ℝ × ℝ × I) := by fun_prop
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
key : Continuous (Y := ℝ × ℝ × (↑I : Type)) fun (x : ℝ × (↑I : Type)) ↦ (t, x)
⊢ Continuous[_, inst] ↿(γ.truncate t)

Tactic:
γ.truncate_continuous_family.comp key

Premises used: Continuous.comp, Path.truncate_continuous_family
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
key : Continuous (Y := ℝ × ℝ × (↑I : Type)) fun (x : ℝ × (↑I : Type)) ↦ (t, x)
⊢ Continuous[_, inst] ↿(γ.truncate t)

Tactic:
exact γ.truncate_continuous_family.comp key

Premises used: Continuous.comp, Path.truncate_continuous_family
-- Module: Mathlib.Topology.Path
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 : ℝ
rw rw₁ : Eq (α := X) ((γ.extend : (a : ℝ) → X) t : X) ((γ.extend : (a : ℝ) → X) t : X)
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) (min t t) : X) ((γ.extend : (a : ℝ) → X) t : X)

Tactic:
rw [min_self]

Premises used: min_self
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
a₁ :
  ∀ (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)
⊢ γ.truncate t t = cast (refl ((γ.extend : (a : ℝ) → X) t)) ⋯ ⋯

Tactic:
ext x
-- Module: Mathlib.Topology.Path
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)
neg :
  ∀ (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)

Tactic:
by_cases hx : x ≤ t
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : (↑I : Type)
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)

Tactic:
simp [truncate]

Premises used: Path.truncate
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : (↑I : Type)
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)

Tactic:
simp [truncate]

Premises used: Path.truncate
-- Module: Mathlib.Topology.Path
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
rw₁ rw₂ : a = a
⊢ (γ.extend : (a : ℝ) → X) (min 0 0) = a

Tactic:
rw [min_self, γ.extend_zero]

Premises used: min_self, Path.extend_zero
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
⊢ Eq (α := Path (X := X) ((γ.extend : (a : ℝ) → X) (min 0 0) : X) ((γ.extend : (a : ℝ) → X) 0 : X)) (γ.truncate 0 0)
    (cast (refl ((γ.extend : (a : ℝ) → X) 0)) ⋯ ⋯)

Tactic:
γ.truncate_self 0

Premises used: Path.truncate_self, OfNat.ofNat
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
⊢ γ.truncate 0 0 = cast (refl a) ⋯ ⋯

Tactic:
convert! γ.truncate_self 0

Premises used: Path.truncate_self, OfNat.ofNat
-- Module: Mathlib.Topology.Path
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
rw₁ rw₂ : b = b
⊢ (γ.extend : (a : ℝ) → X) (min 1 1) = b

Tactic:
rw [min_self, γ.extend_one]

Premises used: min_self, Path.extend_one
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
⊢ Eq (α := Path (X := X) ((γ.extend : (a : ℝ) → X) (min 1 1) : X) ((γ.extend : (a : ℝ) → X) 1 : X)) (γ.truncate 1 1)
    (cast (refl ((γ.extend : (a : ℝ) → X) 1)) ⋯ ⋯)

Tactic:
γ.truncate_self 1

Premises used: Path.truncate_self, OfNat.ofNat
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
⊢ γ.truncate 1 1 = cast (refl b) ⋯ ⋯

Tactic:
convert! γ.truncate_self 1

Premises used: Path.truncate_self, OfNat.ofNat
-- Module: Mathlib.Topology.Path
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 1) = a

Tactic:
simp
-- Module: Mathlib.Topology.Path
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) 1 = b

Tactic:
simp
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
a₁ :
  ∀ (x : (↑I : Type)),
    Eq (α := X) ((γ.truncate 0 1 : (a : (↑I : Type)) → X) x : X) ((γ.cast ⋯ ⋯ : (a : (↑I : Type)) → X) x : X)
⊢ γ.truncate 0 1 = γ.cast ⋯ ⋯

Tactic:
ext x
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
x : (↑I : Type)
a₁ : Eq (α := X) ((γ.truncate 0 1 : (a : (↑I : Type)) → X) x : X) ((γ : (a : (↑I : Type)) → X) x : X)
⊢ Eq (α := X) ((γ.truncate 0 1 : (a : (↑I : Type)) → X) x : X) ((γ.cast ⋯ ⋯ : (a : (↑I : Type)) → X) x : X)

Tactic:
rw [cast_coe]

Premises used: Path.cast_coe