awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
inr :
  Eq (α := X) ((γ₁.trans γ₂ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : X)
    ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
inr₁ :
  Eq (α := X)
    (if h : (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ) ≤ 1 / 2 then
        (γ₁ : (a : (↑I : Type)) → X)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ)) ⋯)
      else
        (γ₂ : (a : (↑I : Type)) → X)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ) - 1) ⋯) :
      X)
    ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
inr₂ :
  Eq (α := X)
    ((γ₁ : (a : (↑I : Type)) → X)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ)) ⋯) :
      X)
    ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
inr₃ : (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ) ≤ 1 / 2
inr₄ :
  Eq (α := X)
    ((γ₁ : (a : (↑I : Type)) → X)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ⋯) : ℝ)) ⋯) :
      X)
    ((γ₁ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * t) ⋯) : X)
⊢ Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X) ((γ₁.extend : (a : ℝ) → X) (2 * t) : X)
have inr₅ : Membership.mem (γ := Set ℝ) (Icc 0 1) (2 * t)
Tactic: rwa [extend_apply _ ⟨ht₀, by linarith⟩, trans_apply, dif_pos, extend_apply]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
| (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X)
have rw : (((γ₁.trans γ₂).extend : (a : ℝ) → X) (1 - (1 - t)) : X)
Tactic: rw [← sub_sub_cancel 1 t]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
⊢ Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) t : X) ((γ₂.extend : (a : ℝ) → X) (2 * t - 1) : X)
have conv_lhs : Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) (1 - (1 - t)) : X) ((γ₂.extend : (a : ℝ) → X) (2 * t - 1) : X)
Tactic: conv_lhs => rw [← sub_sub_cancel 1 t]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
⊢ 1 - t ≤ 1 / 2
have linarith : 1 / 2 < 1 - t → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
linarith : 1 / 2 < 1 - t → 2 / 2 = 1
⊢ 1 - t ≤ 1 / 2
have linarith₁ : 1 / 2 < 1 - t → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
linarith : 1 / 2 < 1 - t → 2 / 2 = 1
linarith₁ : 1 / 2 < 1 - t → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 1 - t ≤ 1 / 2
have linarith₂ : 1 / 2 < 1 - t → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
linarith : 1 / 2 < 1 - t → 2 / 2 = 1
linarith₁ : 1 / 2 < 1 - t → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 / 2 < 1 - t → GT.gt (α := ℝ) 2 0
linarith₃ : 1 / 2 < 1 - t → 2 / 2 = 1
linarith₄ : 1 / 2 < 1 - t → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : 1 / 2 < 1 - t → GT.gt (α := ℝ) 2 0
⊢ 1 - t ≤ 1 / 2
have linarith₆ : 1 / 2 < 1 - t → HMul.hMul (α := ℝ) 1 1 - 2 * t + (HMul.hMul (α := ℝ) 1 1 - (HMul.hMul (α := ℝ) 2 1 - 2 * t)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
⊢ Eq (α := X) (((γ₁.trans γ₂).extend : (a : ℝ) → X) (1 - (1 - t)) : X) ((γ₂.extend : (a : ℝ) → X) (2 * t - 1) : X)
have rw : Eq (α := X) ((γ₂.extend : (a : ℝ) → X) (1 - 2 * (1 - t)) : X) ((γ₂.extend : (a : ℝ) → X) (2 * t - 1) : X)
Tactic: rw [← extend_symm_apply, trans_symm, extend_trans_of_le_half _ _ (by linarith), extend_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
⊢ Eq (α := X) ((γ₂.extend : (a : ℝ) → X) (1 - 2 * (1 - t)) : X) ((γ₂.extend : (a : ℝ) → X) (2 * t - 1) : X)
have h : 1 - 2 * (1 - t) = 2 * t - 1
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
⊢ 1 - 2 * (1 - t) = 2 * t - 1
have linarith : 1 - 2 * (1 - t) < 2 * t - 1 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
linarith : 1 - 2 * (1 - t) < 2 * t - 1 → 2 / 2 = 1
⊢ 1 - 2 * (1 - t) = 2 * t - 1
have linarith₁ : 1 - 2 * (1 - t) < 2 * t - 1 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
linarith : 1 - 2 * (1 - t) < 2 * t - 1 → 2 / 2 = 1
linarith₁ : 1 - 2 * (1 - t) < 2 * t - 1 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 1 - 2 * (1 - t) = 2 * t - 1
have linarith₂ : 1 - 2 * (1 - t) < 2 * t - 1 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
linarith : 1 - 2 * (1 - t) < 2 * t - 1 → 2 / 2 = 1
linarith₁ : 1 - 2 * (1 - t) < 2 * t - 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 - 2 * (1 - t) < 2 * t - 1 → GT.gt (α := ℝ) 2 0
⊢ 1 - 2 * (1 - t) = 2 * t - 1
have linarith₃ : 1 - 2 * (1 - t) < 2 * t - 1 → 1 - 2 * (1 - t) - (2 * t - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
linarith : 1 - 2 * (1 - t) < 2 * t - 1 → 2 / 2 = 1
linarith₁ : 1 - 2 * (1 - t) < 2 * t - 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 - 2 * (1 - t) < 2 * t - 1 → GT.gt (α := ℝ) 2 0
linarith₃ : 1 - 2 * (1 - t) < 2 * t - 1 → 1 - 2 * (1 - t) - (2 * t - 1) = 0
⊢ 1 - 2 * (1 - t) = 2 * t - 1
have linarith₄ : 2 * t - 1 < 1 - 2 * (1 - t) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
linarith : 1 - 2 * (1 - t) < 2 * t - 1 → 2 / 2 = 1
linarith₁ : 1 - 2 * (1 - t) < 2 * t - 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 - 2 * (1 - t) < 2 * t - 1 → GT.gt (α := ℝ) 2 0
linarith₃ : 1 - 2 * (1 - t) < 2 * t - 1 → 1 - 2 * (1 - t) - (2 * t - 1) = 0
linarith₄ : 2 * t - 1 < 1 - 2 * (1 - t) → 2 / 2 = 1
⊢ 1 - 2 * (1 - t) = 2 * t - 1
have linarith₅ : 2 * t - 1 < 1 - 2 * (1 - t) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
linarith : 1 - 2 * (1 - t) < 2 * t - 1 → 2 / 2 = 1
linarith₁ : 1 - 2 * (1 - t) < 2 * t - 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 - 2 * (1 - t) < 2 * t - 1 → GT.gt (α := ℝ) 2 0
linarith₃ : 1 - 2 * (1 - t) < 2 * t - 1 → 1 - 2 * (1 - t) - (2 * t - 1) = 0
linarith₄ : 2 * t - 1 < 1 - 2 * (1 - t) → 2 / 2 = 1
linarith₅ : 2 * t - 1 < 1 - 2 * (1 - t) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 1 - 2 * (1 - t) = 2 * t - 1
have linarith₆ : 2 * t - 1 < 1 - 2 * (1 - t) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
linarith : 1 - 2 * (1 - t) < 2 * t - 1 → 2 / 2 = 1
linarith₁ : 1 - 2 * (1 - t) < 2 * t - 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 - 2 * (1 - t) < 2 * t - 1 → GT.gt (α := ℝ) 2 0
linarith₃ : 1 - 2 * (1 - t) < 2 * t - 1 → 1 - 2 * (1 - t) - (2 * t - 1) = 0
linarith₄ : 2 * t - 1 < 1 - 2 * (1 - t) → 2 / 2 = 1
linarith₅ : 2 * t - 1 < 1 - 2 * (1 - t) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : 2 * t - 1 < 1 - 2 * (1 - t) → GT.gt (α := ℝ) 2 0
⊢ 1 - 2 * (1 - t) = 2 * t - 1
have linarith₇ : 2 * t - 1 < 1 - 2 * (1 - t) → 2 * t - 1 - (1 - 2 * (1 - t)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a : X
⊢ Eq (α := Path a a) (trans (refl a) (refl a)) (refl a)
have a₁ : ∀ (x : (↑I : Type)),
  Eq (α := X) ((trans (refl a) (refl a) : (a : (↑I : Type)) → X) x : X) ((refl a : (a : (↑I : Type)) → X) x : X)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ₁.trans γ₂) : (a : (↑I : Type)) → X))
    (range (ι := (↑I : Type)) (⇑γ₁ : (a : (↑I : Type)) → X) ∪ range (ι := (↑I : Type)) (⇑γ₂ : (a : (↑I : Type)) → X))
have rw : Eq (α := Set X)
  ((⇑γ₁.extend : (a : ℝ) → X) '' HMul.hMul (α := ℝ) 2 '' Iic (1 / 2) ∪
    image (α := ℝ) (⇑γ₂.extend : (a : ℝ) → X) ((fun (x : ℝ) ↦ x - 1) '' HMul.hMul (α := ℝ) 2 '' Ici (1 / 2)))
  (range (ι := (↑I : Type)) (⇑γ₁ : (a : (↑I : Type)) → X) ∪ range (ι := (↑I : Type)) (⇑γ₂ : (a : (↑I : Type)) → X))
Tactic: rw [← extend_range, ← image_univ, ← Iic_union_Ici (a := 1 / 2), image_union,
    EqOn.image_eq fun t ht ↦ extend_trans_of_le_half _ _ (mem_Iic.1 ht),
    EqOn.image_eq fun t ht ↦ extend_trans_of_half_le _ _ (mem_Ici.1 ht),
    ← image_image γ₁.extend, ← image_image (γ₂.extend <| · - 1), ← image_image γ₂.extend]
-- 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 : X
γ : Path x y
f : X → Y
h : Continuous[inst, inst_1] f
⊢ Eq (α := (a : (↑I : Type)) → Y) (⇑(γ.map h) : (a : (↑I : Type)) → Y) (f ∘ (⇑γ : (a : (↑I : Type)) → X))
have h₁ : ∀ (t : (↑I : Type)), (γ.map h : (a : (↑I : Type)) → Y) t = (f ∘ (⇑γ : (a : (↑I : Type)) → X)) t
Tactic: ext 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
γ : Path x y
γ' : Path y z
f : X → Y
h : Continuous[inst, inst_1] f
⊢ (γ.trans γ').map h = (γ.map h).trans (γ'.map h)
have a : ∀ (t : (↑I : Type)),
  Eq (α := Y) (((γ.trans γ').map h : (a : (↑I : Type)) → Y) t : Y)
    (((γ.map h).trans (γ'.map h) : (a : (↑I : Type)) → Y) t : Y)
Tactic: ext 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
γ : Path x y
γ' : Path y z
f : X → Y
h : Continuous[inst, inst_1] f
t : (↑I : Type)
⊢ Eq (α := Y) (((γ.trans γ').map h : (a : (↑I : Type)) → Y) t : Y)
    (((γ.map h).trans (γ'.map h) : (a : (↑I : Type)) → Y) t : Y)
have a : f
    (if h : (↑t : ℝ) ≤ 1 / 2 then (γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) sorry)
    else (γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) sorry)) =
  if h : (↑t : ℝ) ≤ 1 / 2 then
    (f ∘ (⇑γ : (a : (↑I : Type)) → X)) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) sorry)
  else (f ∘ (⇑γ' : (a : (↑I : Type)) → X)) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) sorry)
Tactic: rw [trans_apply, map_coe, Function.comp_apply, trans_apply, map_coe, map_coe]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ γ.map ⋯ = γ
have a : ∀ (x_1 : (↑I : Type)), Eq (α := X) ((γ.map sorry : (a : (↑I : Type)) → X) x_1 : X) ((γ : (a : (↑I : Type)) → X) x_1 : X)
Tactic: ext
-- 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 : X
γ : Path x y
Z : Type u_4
inst_2 : TopologicalSpace Z
f : X → Y
hf : Continuous[inst, inst_1] f
g : Y → Z
hg : Continuous[inst_1, inst_2] g
⊢ (γ.map hf).map hg = γ.map ⋯
have a : ∀ (x_1 : (↑I : Type)),
  Eq (α := Z) (((γ.map hf).map hg : (a : (↑I : Type)) → Z) x_1 : Z) ((γ.map sorry : (a : (↑I : Type)) → Z) x_1 : Z)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y x' y' : X
hx : x' = x
hy : y' = y
⊢ Bijective (β := Path x' y') fun (x_1 : Path x y) ↦ x_1.cast hx hy
have subst_vars : Bijective (β := Path x' y') fun (x : Path x' y') ↦ x.cast sorry sorry
Tactic: subst_vars
Cleared hypotheses: x, y, hx, hy
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_4
inst_1 : TopologicalSpace ι
a b : ι → X
γ : (t : ι) → Path (a t) (b t)
h : Continuous[instTopologicalSpaceProd, inst] ↿γ
⊢ Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ t).extend : (a : ℝ) → X))
have apply : LE.le (α := ℝ) 0 1
Tactic: apply h.comp (continuous_id.prodMap continuous_projIcc)
-- Lean 4 proof step from Mathlib.Topology.Path (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_4
inst_1 : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst] ↿γ₂
⊢ Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → Path (a t) (c t)) fun (t : ι) ↦ (γ₁ t).trans (γ₂ t))
have h₁' : Continuous[instTopologicalSpaceProd, inst]
  (HasUncurry.uncurry (α := (t : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ₁ t).extend : (a : ℝ) → X))
Tactic: have h₁' := Path.continuous_uncurry_extend_of_continuous_family γ₁ h₁
-- Lean 4 proof step from Mathlib.Topology.Path (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_4
inst_1 : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst] ↿γ₂
h₁' :
  Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ₁ t).extend : (a : ℝ) → X))
⊢ Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → Path (a t) (c t)) fun (t : ι) ↦ (γ₁ t).trans (γ₂ t))
have h₂' : Continuous[instTopologicalSpaceProd, inst]
  (HasUncurry.uncurry (α := (t : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ₂ t).extend : (a : ℝ) → X))
Tactic: have h₂' := Path.continuous_uncurry_extend_of_continuous_family γ₂ h₂
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_4
inst_1 : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst] ↿γ₂
h₁' :
  Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ₁ t).extend : (a : ℝ) → X))
h₂' :
  Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ₂ t).extend : (a : ℝ) → X))
⊢ Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → Path (a t) (c t)) fun (t : ι) ↦ (γ₁ t).trans (γ₂ t))
have simp : Continuous[instTopologicalSpaceProd, inst] fun (p : ι × (↑I : Type)) ↦
  ({
        toFun :=
          (fun (t : ℝ) ↦
              if t ≤ 1 / 2 then (extend (x := a p.1) (γ₁ p.1) : (a : ℝ) → X) (2 * t)
              else (extend (x := b p.1) (γ₂ p.1) : (a : ℝ) → X) (2 * t - 1)) ∘
            Subtype.val (p := fun (x : ℝ) ↦ x ∈ I),
        continuous_toFun := sorry, source' := sorry, target' := sorry : Path (a p.1) (c p.1) } :
      (a : (↑I : Type)) → X)
    p.2
Tactic: simp only [HasUncurry.uncurry, Path.trans]
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_4
inst_1 : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst] ↿γ₂
h₁' :
  Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ₁ t).extend : (a : ℝ) → X))
h₂' :
  Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ₂ t).extend : (a : ℝ) → X))
⊢ Continuous[instTopologicalSpaceProd, inst] fun (p : ι × (↑I : Type)) ↦
    ({
          toFun :=
            (fun (t : ℝ) ↦
                if t ≤ 1 / 2 then (extend (x := a p.1) (γ₁ p.1) : (a : ℝ) → X) (2 * t)
                else (extend (x := b p.1) (γ₂ p.1) : (a : ℝ) → X) (2 * t - 1)) ∘
              Subtype.val (p := fun (x : ℝ) ↦ x ∈ I),
          continuous_toFun := ⋯, source' := ⋯, target' := ⋯ : Path (a p.1) (c p.1) } :
        (a : (↑I : Type)) → X)
      p.2
have refine_1 : Continuous[instTopologicalSpaceProd, inst] fun (p : ι × (↑I : Type)) ↦
  (extend (x := a p.1) (γ₁ p.1) : (a : ℝ) → X) (2 * (↑p.2 : ℝ))
Tactic: refine Continuous.if_le ?_ ?_ (continuous_subtype_val.comp continuous_snd) continuous_const ?_
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_4
inst_1 : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst] ↿γ₂
h₁' :
  Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ₁ t).extend : (a : ℝ) → X))
h₂' :
  Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ₂ t).extend : (a : ℝ) → X))
refine_1 :
  Continuous[instTopologicalSpaceProd, inst] fun (p : ι × (↑I : Type)) ↦
    (extend (x := a p.1) (γ₁ p.1) : (a : ℝ) → X) (2 * (↑p.2 : ℝ))
⊢ Continuous[instTopologicalSpaceProd, inst] fun (p : ι × (↑I : Type)) ↦
    ({
          toFun :=
            (fun (t : ℝ) ↦
                if t ≤ 1 / 2 then (extend (x := a p.1) (γ₁ p.1) : (a : ℝ) → X) (2 * t)
                else (extend (x := b p.1) (γ₂ p.1) : (a : ℝ) → X) (2 * t - 1)) ∘
              Subtype.val (p := fun (x : ℝ) ↦ x ∈ I),
          continuous_toFun := ⋯, source' := ⋯, target' := ⋯ : Path (a p.1) (c p.1) } :
        (a : (↑I : Type)) → X)
      p.2
have refine_2 : Continuous[instTopologicalSpaceProd, inst] fun (p : ι × (↑I : Type)) ↦
  (extend (x := b p.1) (γ₂ p.1) : (a : ℝ) → X) (2 * (↑p.2 : ℝ) - 1)
Tactic: refine Continuous.if_le ?_ ?_ (continuous_subtype_val.comp continuous_snd) continuous_const ?_
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_4
inst_1 : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst] ↿γ₂
h₁' :
  Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ₁ t).extend : (a : ℝ) → X))
h₂' :
  Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ₂ t).extend : (a : ℝ) → X))
refine_1 :
  Continuous[instTopologicalSpaceProd, inst] fun (p : ι × (↑I : Type)) ↦
    (extend (x := a p.1) (γ₁ p.1) : (a : ℝ) → X) (2 * (↑p.2 : ℝ))
refine_2 :
  Continuous[instTopologicalSpaceProd, inst] fun (p : ι × (↑I : Type)) ↦
    (extend (x := b p.1) (γ₂ p.1) : (a : ℝ) → X) (2 * (↑p.2 : ℝ) - 1)
⊢ Continuous[instTopologicalSpaceProd, inst] fun (p : ι × (↑I : Type)) ↦
    ({
          toFun :=
            (fun (t : ℝ) ↦
                if t ≤ 1 / 2 then (extend (x := a p.1) (γ₁ p.1) : (a : ℝ) → X) (2 * t)
                else (extend (x := b p.1) (γ₂ p.1) : (a : ℝ) → X) (2 * t - 1)) ∘
              Subtype.val (p := fun (x : ℝ) ↦ x ∈ I),
          continuous_toFun := ⋯, source' := ⋯, target' := ⋯ : Path (a p.1) (c p.1) } :
        (a : (↑I : Type)) → X)
      p.2
have refine_3 : ∀ (x : ι × (↑I : Type)),
  (↑x.2 : ℝ) = 1 / 2 →
    Eq (α := X) ((extend (x := a x.1) (γ₁ x.1) : (a : ℝ) → X) (2 * (↑x.2 : ℝ)) : X)
      ((extend (x := b x.1) (γ₂ x.1) : (a : ℝ) → X) (2 * (↑x.2 : ℝ) - 1) : X)
Tactic: refine Continuous.if_le ?_ ?_ (continuous_subtype_val.comp continuous_snd) continuous_const ?_
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_4
inst_1 : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst] ↿γ₂
h₁' :
  Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ₁ t).extend : (a : ℝ) → X))
h₂' :
  Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ₂ t).extend : (a : ℝ) → X))
⊢ Continuous[instTopologicalSpaceProd, inst] fun (p : ι × (↑I : Type)) ↦
    (extend (x := a p.1) (γ₁ p.1) : (a : ℝ) → X) (2 * (↑p.2 : ℝ))
have refine_1 : Continuous[instTopologicalSpaceProd, inst]
  ((fun (p : ι × ℝ) ↦ (extend (x := a p.1) (γ₁ p.1) : (a : ℝ) → X) p.2) ∘
    Prod.map id fun (x : (↑I : Type)) ↦ 2 * (↑x : ℝ))
Tactic: change
      Continuous ((fun p : ι × ℝ => (γ₁ p.1).extend p.2) ∘ Prod.map id (fun x => 2 * x : I → ℝ))
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_4
inst_1 : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst] ↿γ₂
h₁' :
  Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ₁ t).extend : (a : ℝ) → X))
h₂' :
  Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ₂ t).extend : (a : ℝ) → X))
⊢ Continuous[instTopologicalSpaceProd, inst] fun (p : ι × (↑I : Type)) ↦
    (extend (x := b p.1) (γ₂ p.1) : (a : ℝ) → X) (2 * (↑p.2 : ℝ) - 1)
have refine_2 : Continuous[instTopologicalSpaceProd, inst]
  ((fun (p : ι × ℝ) ↦ (extend (x := b p.1) (γ₂ p.1) : (a : ℝ) → X) p.2) ∘
    Prod.map id fun (x : (↑I : Type)) ↦ 2 * (↑x : ℝ) - 1)
Tactic: change
      Continuous ((fun p : ι × ℝ => (γ₂ p.1).extend p.2) ∘ Prod.map id (fun x => 2 * x - 1 : I → ℝ))
-- 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
f : Y → Path x y
g : Y → Path y z
hf : Continuous[inst_1, _] f
hg : Continuous[inst_1, _] g
⊢ Continuous[inst_1, _] fun (t : Y) ↦ (f t).trans (g t)
have apply : Continuous[instTopologicalSpaceProd, inst] (HasUncurry.uncurry (α := Y → Path x z) fun (t : Y) ↦ (f t).trans (g t))
Tactic: apply continuous_uncurry_iff.mp
-- 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)
⊢ (Path.pi (χ := χ) γ₀).trans (Path.pi (χ := χ) γ₁) = Path.pi (χ := χ) fun (i : ι) ↦ (γ₀ i).trans (γ₁ i)
have a : ∀ (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)
Tactic: ext t i