awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Path
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)
a :
  f
      (if h : (↑t : ℝ) ≤ 1 / 2 then (γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯)
      else (γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯)) =
    if h : (↑t : ℝ) ≤ 1 / 2 then
      (f ∘ (⇑γ : (a : (↑I : Type)) → X)) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯)
    else (f ∘ (⇑γ' : (a : (↑I : Type)) → X)) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯)
⊢ Eq (α := Y) (((γ.trans γ').map h : (a : (↑I : Type)) → Y) t : Y)
    (((γ.map h).trans (γ'.map h) : (a : (↑I : Type)) → Y) t : Y)

Tactic:
rw [trans_apply, map_coe, Function.comp_apply, trans_apply, map_coe, map_coe]

Premises used: Path.trans_apply, Path.map_coe, Function.comp_apply
-- Module: Mathlib.Topology.Path
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)
⊢ f
      (if h : (↑t : ℝ) ≤ 1 / 2 then (γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯)
      else (γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯)) =
    if h : (↑t : ℝ) ≤ 1 / 2 then
      (f ∘ (⇑γ : (a : (↑I : Type)) → X)) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯)
    else (f ∘ (⇑γ' : (a : (↑I : Type)) → X)) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯)

Tactic:
grind
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
a : ∀ (x_1 : (↑I : Type)), Eq (α := X) ((γ.map ⋯ : (a : (↑I : Type)) → X) x_1 : X) ((γ : (a : (↑I : Type)) → X) x_1 : X)
⊢ γ.map ⋯ = γ

Tactic:
ext
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
x_1 : (↑I : Type)
⊢ Eq (α := X) ((γ.map ⋯ : (a : (↑I : Type)) → X) x_1 : X) ((γ : (a : (↑I : Type)) → X) x_1 : X)

Tactic:
rfl
-- Module: Mathlib.Topology.Path
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
a :
  ∀ (x_1 : (↑I : Type)),
    Eq (α := Z) (((γ.map hf).map hg : (a : (↑I : Type)) → Z) x_1 : Z) ((γ.map ⋯ : (a : (↑I : Type)) → Z) x_1 : Z)
⊢ (γ.map hf).map hg = γ.map ⋯

Tactic:
ext
-- Module: Mathlib.Topology.Path
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
x_1 : (↑I : Type)
⊢ Eq (α := Z) (((γ.map hf).map hg : (a : (↑I : Type)) → Z) x_1 : Z) ((γ.map ⋯ : (a : (↑I : Type)) → Z) x_1 : Z)

Tactic:
rfl
-- 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
x' y' : X
hx : x' = x
hy : y' = y
⊢ (γ : (a : (↑I : Type)) → X) 0 = x'

Tactic:
simp [hx]
-- 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
x' y' : X
hx : x' = x
hy : y' = y
⊢ (γ : (a : (↑I : Type)) → X) 1 = y'

Tactic:
simp [hy]
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ γ.cast ⋯ ⋯ = γ

Tactic:
rfl

Premises used: Path.cast, rfl
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a₁ a₂ b₁ b₂ : X
γ : Path a₂ b₂
ha : a₁ = a₂
hb : b₁ = b₂
⊢ γ.symm.cast hb ha = (γ.cast ha hb).symm

Tactic:
rfl

Premises used: Path.symm, rfl
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a₁ a₂ b₁ b₂ c₁ c₂ : X
γ : Path a₂ b₂
γ' : Path b₂ c₂
ha : a₁ = a₂
hb : b₁ = b₂
hc : c₁ = c₂
⊢ (γ.trans γ').cast ha hc = (γ.cast ha hb).trans (γ'.cast hb hc)

Tactic:
rfl

Premises used: Path.trans, Path.cast, rfl, ite
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y x' y' : X
γ : Path x y
hx : x' = x
hy : y' = y
⊢ (γ.cast hx hy).extend = γ.extend

Tactic:
rfl

Premises used: Path.cast, Path.extend, rfl
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
x' y' : X
hx : x' = x
hy : y' = y
⊢ Eq (α := (a : (↑I : Type)) → X) (⇑(γ.cast hx hy) : (a : (↑I : Type)) → X) (⇑γ : (a : (↑I : Type)) → X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y x' y' : X
hx : x' = x
hy : y' = y
subst_vars : Bijective (β := Path x' y') fun (x : Path x' y') ↦ x.cast ⋯ ⋯
⊢ Bijective (β := Path x' y') fun (x_1 : Path x y) ↦ x_1.cast hx hy

Tactic:
subst_vars
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x' y' : X
⊢ Bijective (β := Path x' y') fun (x : Path x' y') ↦ x.cast ⋯ ⋯

Tactic:
bijective_id

Premises used: Function.bijective_id, Path.cast
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x' y' : X
⊢ Bijective (β := Path x' y') fun (x : Path x' y') ↦ x.cast ⋯ ⋯

Tactic:
exact bijective_id

Premises used: Function.bijective_id
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x₁ x₂ y₁ y₂ : X
p : Path x₁ y₁ → Prop
hx : x₁ = x₂
hy : y₁ = y₂
⊢ (∃ (γ : Path x₁ y₁), p γ) ↔ ∃ (γ : Path x₂ y₂), p (γ.cast hx hy)

Tactic:
bijective_cast hx hy |>.surjective.exists

Premises used: Path.bijective_cast, Function.Surjective.exists, Function.Bijective.surjective
-- Module: Mathlib.Topology.Path
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 : ι) → Path (b t) (a t)) fun (t : ι) ↦ (γ t).symm)

Tactic:
h.comp (continuous_id.prodMap continuous_symm)

Premises used: Continuous.prodMap, Continuous.comp, continuous_id, unitInterval.symm, unitInterval.continuous_symm
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ Continuous[_, inst] (HasUncurry.uncurry (α := (t : Path x y) → Path x y) fun (t : Path x y) ↦ t)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Path
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] ↿γ
apply : LE.le (α := ℝ) 0 1
⊢ Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ t).extend : (a : ℝ) → X))

Tactic:
apply h.comp (continuous_id.prodMap continuous_projIcc)

Premises used: Continuous.prodMap, Continuous.comp, continuous_id, continuous_projIcc
-- Module: Mathlib.Topology.Path
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] ↿γ
⊢ LE.le (α := ℝ) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Topology.Path
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] ↿γ
⊢ LE.le (α := ℝ) 0 1

Tactic:
exact zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Topology.Path
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 : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ₁ t).extend : (a : ℝ) → X))

Tactic:
have h₁' := Path.continuous_uncurry_extend_of_continuous_family γ₁ h₁
-- Module: Mathlib.Topology.Path
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 : ι) → (a : ℝ) → X) fun (t : ι) ↦ (⇑(γ₂ t).extend : (a : ℝ) → X))

Tactic:
have h₂' := Path.continuous_uncurry_extend_of_continuous_family γ₂ h₂
-- Module: Mathlib.Topology.Path
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))
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 := ⋯, source' := ⋯, target' := ⋯ : Path (a p.1) (c p.1) } :
        (a : (↑I : Type)) → X)
      p.2
⊢ Continuous[instTopologicalSpaceProd, inst]
    (HasUncurry.uncurry (α := (t : ι) → Path (a t) (c t)) fun (t : ι) ↦ (γ₁ t).trans (γ₂ t))

Tactic:
simp only [HasUncurry.uncurry, Path.trans]

Premises used: Path.trans, Function.HasUncurry.uncurry
-- Module: Mathlib.Topology.Path
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

Tactic:
Continuous.if_le ?_ ?_ (continuous_subtype_val.comp continuous_snd) continuous_const ?_

Premises used: continuous_subtype_val, Continuous.comp, continuous_const, continuous_snd, Continuous.if_le, ite
-- Module: Mathlib.Topology.Path
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)
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)
⊢ 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

Tactic:
refine Continuous.if_le ?_ ?_ (continuous_subtype_val.comp continuous_snd) continuous_const ?_

Premises used: continuous_subtype_val, Continuous.comp, continuous_const, continuous_snd, Continuous.if_le
-- Module: Mathlib.Topology.Path
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 : ι × ℝ) ↦ (extend (x := a p.1) (γ₁ p.1) : (a : ℝ) → X) p.2) ∘
      Prod.map id fun (x : (↑I : Type)) ↦ 2 * (↑x : ℝ))
⊢ Continuous[instTopologicalSpaceProd, inst] fun (p : ι × (↑I : Type)) ↦
    (extend (x := a p.1) (γ₁ p.1) : (a : ℝ) → X) (2 * (↑p.2 : ℝ))

Tactic:
change
      Continuous ((fun p : ι × ℝ => (γ₁ p.1).extend p.2) ∘ Prod.map id (fun x => 2 * x : I → ℝ))

Premises used: Continuous, HMul.hMul, Function.comp, id, Prod.map, Prod.fst, Path.extend, OfNat.ofNat, Subtype.val, Prod.snd, DFunLike.coe
-- Module: Mathlib.Topology.Path
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, instTopologicalSpaceProd] (Prod.map id fun (x : (↑I : Type)) ↦ 2 * (↑x : ℝ))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Path
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 : ι × ℝ) ↦ (extend (x := a p.1) (γ₁ p.1) : (a : ℝ) → X) p.2) ∘
      Prod.map id fun (x : (↑I : Type)) ↦ 2 * (↑x : ℝ))

Tactic:
exact h₁'.comp (by fun_prop)

Premises used: Continuous.comp
-- Module: Mathlib.Topology.Path
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_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)
⊢ Continuous[instTopologicalSpaceProd, inst] fun (p : ι × (↑I : Type)) ↦
    (extend (x := b p.1) (γ₂ p.1) : (a : ℝ) → X) (2 * (↑p.2 : ℝ) - 1)

Tactic:
change
      Continuous ((fun p : ι × ℝ => (γ₂ p.1).extend p.2) ∘ Prod.map id (fun x => 2 * x - 1 : I → ℝ))

Premises used: Continuous, HMul.hMul, HSub.hSub, Function.comp, id, Prod.map, Prod.fst, Path.extend, OfNat.ofNat, Subtype.val, Prod.snd, DFunLike.coe
-- Module: Mathlib.Topology.Path
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, instTopologicalSpaceProd] (Prod.map id fun (x : (↑I : Type)) ↦ 2 * (↑x : ℝ) - 1)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Path
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 : ι × ℝ) ↦ (extend (x := b p.1) (γ₂ p.1) : (a : ℝ) → X) p.2) ∘
      Prod.map id fun (x : (↑I : Type)) ↦ 2 * (↑x : ℝ) - 1)

Tactic:
exact h₂'.comp (by fun_prop)

Premises used: Continuous.comp
-- Module: Mathlib.Topology.Path
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))
st : ι × (↑I : Type)
hst : (↑st.2 : ℝ) = 1 / 2
⊢ Eq (α := X) ((extend (x := a st.1) (γ₁ st.1) : (a : ℝ) → X) (2 * (↑st.2 : ℝ)) : X)
    ((extend (x := b st.1) (γ₂ st.1) : (a : ℝ) → X) (2 * (↑st.2 : ℝ) - 1) : X)

Tactic:
simp [hst]
-- Module: Mathlib.Topology.Path
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
apply :
  Continuous[instTopologicalSpaceProd, inst] (HasUncurry.uncurry (α := Y → Path x z) fun (t : Y) ↦ (f t).trans (g t))
⊢ Continuous[inst_1, _] fun (t : Y) ↦ (f t).trans (g t)

Tactic:
apply continuous_uncurry_iff.mp

Premises used: Path.continuous_uncurry_iff, Iff.mp
-- Module: Mathlib.Topology.Path
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[instTopologicalSpaceProd, inst] (HasUncurry.uncurry (α := Y → Path x z) fun (t : Y) ↦ (f t).trans (g t))

Tactic:
trans_continuous_family _ (continuous_uncurry_iff.mpr hf) _ (continuous_uncurry_iff.mpr hg)

Premises used: Iff.mpr, Path.continuous_uncurry_iff, Path.trans_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
f : Y → Path x y
g : Y → Path y z
hf : Continuous[inst_1, _] f
hg : Continuous[inst_1, _] g
⊢ Continuous[instTopologicalSpaceProd, inst] (HasUncurry.uncurry (α := Y → Path x z) fun (t : Y) ↦ (f t).trans (g t))

Tactic:
exact trans_continuous_family _ (continuous_uncurry_iff.mpr hf) _ (continuous_uncurry_iff.mpr hg)

Premises used: Iff.mpr, Path.continuous_uncurry_iff, Path.trans_continuous_family
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
⊢ Continuous (Y := Path x z) fun (ρ : Path x y × Path y z) ↦ ρ.1.trans ρ.2

Tactic:
fun_prop
-- 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
γ : Path x y
a₁ a₂ a₃ : X
b₁ b₂ b₃ : Y
γ₁ : Path a₁ a₂
γ₂ : Path b₁ b₂
⊢ (γ₁.prodMk γ₂.toContinuousMap).toFun 0 = (a₁, b₁)

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
γ : Path x y
a₁ a₂ a₃ : X
b₁ b₂ b₃ : Y
γ₁ : Path a₁ a₂
γ₂ : Path b₁ b₂
⊢ (γ₁.prodMk γ₂.toContinuousMap).toFun 1 = (a₂, b₂)

Tactic:
simp
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
a₁ a₂ : X
b₁ b₂ : Y
γ₁ : Path a₁ a₂
γ₂ : Path b₁ b₂
⊢ Eq (α := (a : (↑I : Type)) → X × Y) (⇑(γ₁.prod γ₂) : (a : (↑I : Type)) → X × Y) fun (t : (↑I : Type)) ↦
    ((γ₁ : (a : (↑I : Type)) → X) t, (γ₂ : (a : (↑I : Type)) → Y) t)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
a₁ a₂ a₃ : X
b₁ b₂ b₃ : Y
γ₁ : Path a₁ a₂
δ₁ : Path a₂ a₃
γ₂ : Path b₁ b₂
δ₂ : Path b₂ b₃
⊢ (γ₁.prod γ₂).trans (δ₁.prod δ₂) = (γ₁.trans δ₁).prod (γ₂.trans δ₂)

Tactic:
grind
-- 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
χ : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ : (i : ι) → Path (as i) (bs i)
⊢ ContinuousMap.toFun (X := (↑I : Type)) (ContinuousMap.pi (X := χ) fun (i : ι) ↦ (γ i).toContinuousMap) 0 = as

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
χ : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ : (i : ι) → Path (as i) (bs i)
⊢ ContinuousMap.toFun (X := (↑I : Type)) (ContinuousMap.pi (X := χ) fun (i : ι) ↦ (γ i).toContinuousMap) 1 = bs

Tactic:
simp
-- Module: Mathlib.Topology.Path
Goal:
ι : Type u_3
χ : ι → Type u_4
inst : (i : ι) → TopologicalSpace (χ i)
as bs : (i : ι) → χ i
γ : (i : ι) → Path (as i) (bs i)
⊢ Eq (α := (a : (↑I : Type)) → (i : ι) → χ i) (⇑(Path.pi (χ := χ) γ) : (a : (↑I : Type)) → (i : ι) → χ i)
    fun (t : (↑I : Type)) (i : ι) ↦ (γ i : (a : (↑I : Type)) → χ i) t

Tactic:
rfl

Premises used: 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)
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)
⊢ (Path.pi (χ := χ) γ₀).trans (Path.pi (χ := χ) γ₁) = Path.pi (χ := χ) fun (i : ι) ↦ (γ₀ i).trans (γ₁ i)

Tactic:
ext t i