awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen[inst] (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ (i : Fin n), s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate (s := t) s
hfcp : ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
i : Fin n
x : X
⊢ Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)

Tactic:
⟨f.nonneg i x, PartitionOfUnity.le_one f i x⟩

Premises used: Set.Mem, setOf, PartitionOfUnity.nonneg, Set.Icc, And.intro, PartitionOfUnity.le_one
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen[inst] (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ (i : Fin n), s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate (s := t) s
hfcp : ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
i : Fin n
x : X
⊢ Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)

Tactic:
exact ⟨f.nonneg i x, PartitionOfUnity.le_one f i x⟩
-- 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
h :
  Eq.{max 1 (u_1 + 1)} (α := (a : (↑I : Type)) → X)
    ((fun (γ : Path x y) ↦ ((⇑γ.toContinuousMap : (a : (↑I : Type)) → X) : (a : (↑I : Type)) → X)) γ₁)
    ((fun (γ : Path x y) ↦ ((⇑γ.toContinuousMap : (a : (↑I : Type)) → X) : (a : (↑I : Type)) → X)) γ₂)
⊢ γ₁.toContinuousMap = γ₂.toContinuousMap

Tactic:
simp only [DFunLike.coe_fn_eq] at h

Premises used: DFunLike.coe_fn_eq
-- 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
h : γ₁.toContinuousMap = γ₂.toContinuousMap
mk :
  ∀ (toContinuousMap : C((↑I : Type), X)) (source' : toContinuousMap.toFun 0 = x)
    (target' : toContinuousMap.toFun 1 = y)
    (h :
      { toContinuousMap := toContinuousMap, source' := source', target' := target' : Path x y }.toContinuousMap =
        γ₂.toContinuousMap),
    { toContinuousMap := toContinuousMap, source' := source', target' := target' : Path x y } = γ₂
⊢ γ₁ = γ₂

Tactic:
cases γ₁
-- 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
toContinuousMap : C((↑I : Type), X)
source' : toContinuousMap.toFun 0 = x
target' : toContinuousMap.toFun 1 = y
h :
  { toContinuousMap := toContinuousMap, source' := source', target' := target' : Path x y }.toContinuousMap =
    γ₂.toContinuousMap
mk :
  ∀ (toContinuousMap_1 : C((↑I : Type), X)) (source'_1 : toContinuousMap_1.toFun 0 = x)
    (target'_1 : toContinuousMap_1.toFun 1 = y)
    (h :
      { toContinuousMap := toContinuousMap, source' := source', target' := target' : Path x y }.toContinuousMap =
        { toContinuousMap := toContinuousMap_1, source' := source'_1, target' := target'_1 :
            Path x y }.toContinuousMap),
    { toContinuousMap := toContinuousMap, source' := source', target' := target' : Path x y } =
      { toContinuousMap := toContinuousMap_1, source' := source'_1, target' := target'_1 }
⊢ { toContinuousMap := toContinuousMap, source' := source', target' := target' : Path x y } = γ₂

Tactic:
cases γ₂
-- 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
toContinuousMap : C((↑I : Type), X)
source' : toContinuousMap.toFun 0 = x
target' : toContinuousMap.toFun 1 = y
toContinuousMap_1 : C((↑I : Type), X)
source'_1 : toContinuousMap_1.toFun 0 = x
target'_1 : toContinuousMap_1.toFun 1 = y
h :
  { toContinuousMap := toContinuousMap, source' := source', target' := target' : Path x y }.toContinuousMap =
    { toContinuousMap := toContinuousMap_1, source' := source'_1, target' := target'_1 : Path x y }.toContinuousMap
⊢ { toContinuousMap := toContinuousMap, source' := source', target' := target' : Path x y } =
    { toContinuousMap := toContinuousMap_1, source' := source'_1, target' := target'_1 }

Tactic:
congr
-- 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
⊢ Continuous[_, inst] (⇑γ.toContinuousMap : (a : (↑I : Type)) → X)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x_1 y : X
x : (↑I : Type) → X
h11 : Continuous[_, inst] x
h12 : { toFun := x, continuous_toFun := h11 : C((↑I : Type), X) }.toFun 0 = x_1
h13 : { toFun := x, continuous_toFun := h11 : C((↑I : Type), X) }.toFun 1 = y
h21 :
  Continuous[_, inst]
    (⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 : Path x_1 y } : (a : (↑I : Type)) → X)
h22 :
  {
          toFun :=
            (⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 : Path x_1 y } :
              (a : (↑I : Type)) → X),
          continuous_toFun := h21 : C((↑I : Type), X) }.toFun
      0 =
    x_1
h23 :
  {
          toFun :=
            (⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 : Path x_1 y } :
              (a : (↑I : Type)) → X),
          continuous_toFun := h21 : C((↑I : Type), X) }.toFun
      1 =
    y
⊢ { toFun := x, continuous_toFun := h11, source' := h12, target' := h13 : Path x_1 y } =
    {
      toFun :=
        (⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 : Path x_1 y } : (a : (↑I : Type)) → X),
      continuous_toFun := h21, source' := h22, target' := h23 }

Tactic:
rfl
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
f : C((↑I : Type), X)
h₁ : f.toFun 0 = x
h₂ : f.toFun 1 = y
⊢ Eq (α := (a : (↑I : Type)) → X)
    (⇑{ toContinuousMap := f, source' := h₁, target' := h₂ : Path x y } : (a : (↑I : Type)) → X)
    (⇑f : (a : (↑I : Type)) → X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
f : (↑I : Type) → X
h₁ : Continuous[_, inst] f
h₂ : f 0 = x
h₃ : f 1 = y
⊢ (⇑{ toFun := f, continuous_toFun := h₁, source' := h₂, target' := h₃ : Path x y } : (a : (↑I : Type)) → X) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ Continuous[_, inst] (⇑γ : (a : (↑I : Type)) → X)

Tactic:
γ.continuous_toFun

Premises used: ContinuousMap.continuous_toFun, Path.toContinuousMap
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ (γ : (a : (↑I : Type)) → X) 0 = x

Tactic:
γ.source'

Premises used: Path.source'
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ (γ : (a : (↑I : Type)) → X) 1 = y

Tactic:
γ.target'

Premises used: Path.target'
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ Eq (α := (a : (↑I : Type)) → X) (⇑γ.toContinuousMap : (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
⊢ Eq (α := Set C((↑I : Type), X)) (range (ι := Path x y) _root_.toContinuousMap)
    {f : C((↑I : Type), X) | (f : (a : (↑I : Type)) → X) 0 = x ∧ (f : (a : (↑I : Type)) → X) 1 = y}

Tactic:
Subset.antisymm (range_subset_iff.mpr fun γ ↦ ⟨γ.source, γ.target⟩) fun f ⟨hf₀, hf₁⟩ ↦
    ⟨⟨f, hf₀, hf₁⟩, rfl⟩

Premises used: Set.Subset.antisymm, Iff.mpr, _private.0.Path.range_coe.match_1, Membership.mem, toContinuousMap, Path.mk, And.intro, Exists.intro, Path.source, Set.range, Path.target, Set.range_subset_iff, rfl
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) x

Tactic:
⟨0, Path.source γ⟩

Premises used: Set.Mem, setOf, Exists.intro, Path.source, Set.range, OfNat.ofNat
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) y

Tactic:
⟨1, Path.target γ⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, Path.target, OfNat.ofNat
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a : X
⊢ Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(refl a) : (a : (↑I : Type)) → X)) {a}

Tactic:
range_const

Premises used: Set.range_const
-- 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
⊢ Continuous[_, inst] ((⇑γ : (a : (↑I : Type)) → X) ∘ σ)

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
γ_1 γ : Path x y
⊢ ((⇑γ : (a : (↑I : Type)) → X) ∘ σ) 0 = y

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 : (↑I : Type)) → X) ∘ σ) 1 = x

Tactic:
simp
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ γ.symm.symm = γ

Tactic:
grind
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := Path x y) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, Path.symm_symm, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a : X
⊢ Eq (α := Path a a) (symm (refl a)) (refl a)

Tactic:
rfl

Premises used: Path.symm, ContinuousMap.const, Path.refl, rfl
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
⊢ Eq (α := Set X) (range (ι := (↑I : Type)) (⇑γ.symm : (a : (↑I : Type)) → X))
    (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))

Tactic:
symm_involutive.surjective.range_comp γ

Premises used: Function.Involutive.surjective, Function.Surjective.range_comp, unitInterval.symm_involutive, DFunLike.coe
-- 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
⊢ ContinuousEval (Path x y) (↑I : Type) X

Tactic:
.of_continuous_forget continuous_induced_dom

Premises used: continuous_induced_dom, ContinuousEval.of_continuous_forget
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
Y : Type u_4
inst_1 : TopologicalSpace Y
g : Y → Path x y
⊢ Continuous[instTopologicalSpaceProd, inst] ↿g ↔ Continuous[inst_1, _] g

Tactic:
Iff.symm <| continuous_induced_rng.trans
    ⟨fun h => continuous_uncurry_of_continuous ⟨_, h⟩,
    continuous_of_continuous_uncurry (fun (y : Y) ↦ ContinuousMap.mk (g y))⟩

Premises used: ContinuousMap.mk, ContinuousMap.continuous_of_continuous_uncurry, Function.comp, toContinuousMap, ContinuousMap.continuous_uncurry_of_continuous, Iff.intro, Iff.trans, DFunLike.coe, Iff.symm, continuous_induced_rng
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
γ : Y → Path x y
f : Y → ℝ
hγ : Continuous[instTopologicalSpaceProd, inst] ↿γ
hf : Continuous[inst_1, _] f
⊢ Continuous[inst_1, inst] fun (t : Y) ↦ ((γ t).extend : (a : ℝ) → X) (f t)

Tactic:
Continuous.IccExtend hγ hf

Premises used: Continuous.IccExtend, Set.IccExtend
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ Continuous[_, inst] (⇑γ.extend : (a : ℝ) → X)

Tactic:
γ.continuous.Icc_extend'

Premises used: Path.continuous, Set.IccExtend, Continuous.Icc_extend'
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
l r : Y → X
y : Y
l₁ : Filter ℝ
l₂ : Filter X
γ : (y : Y) → Path (l y) (r y)
hγ : Tendsto (↿γ) (SProd.sprod (β := Filter (↑(Icc 0 1) : Type)) (𝓝 y) (map (projIcc 0 1 ⋯) l₁)) l₂
⊢ Tendsto (HasUncurry.uncurry (α := (x : Y) → (a : ℝ) → X) fun (x : Y) ↦ (⇑(γ x).extend : (a : ℝ) → X)) (𝓝 y ×ˢ l₁) l₂

Tactic:
Filter.Tendsto.IccExtend _ hγ

Premises used: Filter.Tendsto.IccExtend, Set.IccExtend
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
g : Y → ℝ
l r : Y → X
γ : (y : Y) → Path (l y) (r y)
y : Y
hγ : ContinuousAt ↿γ (y, projIcc 0 1 ⋯ (g y))
hg : ContinuousAt g y
⊢ ContinuousAt.{u_2, u_1} (Y := X) (fun (i : Y) ↦ ((γ i).extend : (a : ℝ) → X) (g i)) y

Tactic:
hγ.IccExtend (fun x => γ x) hg

Premises used: ContinuousAt.IccExtend, Set.IccExtend, DFunLike.coe
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) t : X)
    ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) t ht) : X)

Tactic:
IccExtend_of_mem _ γ ht

Premises used: Set.Mem, Set.IccExtend_of_mem, Set.IccExtend, DFunLike.coe
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ (γ.extend : (a : ℝ) → X) 0 = x

Tactic:
simp
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ (γ.extend : (a : ℝ) → X) 1 = y

Tactic:
simp
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t : (↑(Icc 0 1) : Type)
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) (↑t : ℝ) : X) ((γ : (a : (↑I : Type)) → X) t : X)

Tactic:
IccExtend_val _ γ t

Premises used: Set.IccExtend_val, Set.IccExtend, DFunLike.coe
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
⊢ Eq (α := Set X) (range (ι := ℝ) (⇑γ.extend : (a : ℝ) → X)) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))

Tactic:
IccExtend_range _ γ

Premises used: Set.IccExtend_range, Set.IccExtend, DFunLike.coe
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
ht : t ≤ 0
⊢ (γ.extend : (a : ℝ) → X) t = a

Tactic:
(IccExtend_of_le_left _ _ ht).trans γ.source

Premises used: Set.IccExtend_of_le_left, Path.source, Set.IccExtend, Eq.trans
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
ht : 1 ≤ t
⊢ (γ.extend : (a : ℝ) → X) t = b

Tactic:
(IccExtend_of_right_le _ _ ht).trans γ.target

Premises used: Set.IccExtend_of_right_le, Set.IccExtend, Path.target, Eq.trans
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
a : X
⊢ Eq (α := C(ℝ, X)) (extend (refl a)) (ContinuousMap.const ℝ a)

Tactic:
rfl

Premises used: Path.extend, ContinuousMap.const, Set.IccExtend, rfl
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
t : ℝ
⊢ Eq (α := X) ((γ.symm.extend : (a : ℝ) → X) t : X) ((γ.extend : (a : ℝ) → X) (1 - t) : X)

Tactic:
congrArg γ <| symm_projIcc _

Premises used: congrArg, unitInterval.symm_projIcc, Set.IccExtend, DFunLike.coe
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ Eq (α := (a : ℝ) → X) (⇑γ.symm.extend : (a : ℝ) → X) fun (x_1 : ℝ) ↦ (γ.extend : (a : ℝ) → X) (1 - x_1)

Tactic:
funext γ.extend_symm_apply

Premises used: Path.extend_symm_apply, funext
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
f : ℝ → X
hf : ContinuousOn f I
h₀ : f 0 = x
h₁ : f 1 = y
⊢ ∀ (t : (↑I : Type)), Membership.mem (α := X) (f '' I) ((ofLine hf h₀ h₁ : (a : (↑I : Type)) → X) t : X)

Tactic:
fun ⟨t, t_in⟩ => ⟨t, t_in, rfl⟩

Premises used: Path.ofLine, Membership.mem, _private.0.Path.ofLine_mem.match_1, And.intro, Exists.intro, Set.image, DFunLike.coe, unitInterval, 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
⊢ ContinuousOn (Y := X) (⇑γ.extend : (a : ℝ) → X) I

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

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

Tactic:
simp [ofLine]

Premises used: Path.ofLine
-- 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
γ' : Path y z
⊢ ∀ (x_1 : ℝ),
    id x_1 = 1 / 2 → Eq (α := X) ((γ.extend : (a : ℝ) → X) (2 * x_1) : X) ((γ'.extend : (a : ℝ) → X) (2 * x_1 - 1) : X)

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
γ' : Path y z
refine_1 : Continuous[_, inst] fun (t : ℝ) ↦ (γ.extend : (a : ℝ) → X) (2 * t)
refine_2 : Continuous[_, inst] fun (t : ℝ) ↦ (γ'.extend : (a : ℝ) → X) (2 * t - 1)
⊢ Continuous[_, inst]
    ((fun (t : ℝ) ↦ if t ≤ 1 / 2 then (γ.extend : (a : ℝ) → X) (2 * t) else (γ'.extend : (a : ℝ) → X) (2 * t - 1)) ∘
      Subtype.val (p := fun (x : ℝ) ↦ x ∈ I))

Tactic:
refine
      (Continuous.if_le ?_ ?_ continuous_id continuous_const (by simp)).comp
        continuous_subtype_val

Premises used: continuous_subtype_val, Continuous.comp, continuous_const, Continuous.if_le, continuous_id
-- 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
γ' : Path y z
⊢ Continuous[_, inst] fun (t : ℝ) ↦ (γ.extend : (a : ℝ) → X) (2 * t)

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
γ_1 γ : Path x y
γ' : Path y z
⊢ Continuous[_, inst] fun (t : ℝ) ↦ (γ'.extend : (a : ℝ) → X) (2 * t - 1)

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
γ_1 γ : Path x y
γ' : Path y z
⊢ Function.comp (α := (↑I : Type))
      (fun (t : ℝ) ↦ if t ≤ 1 / 2 then (γ.extend : (a : ℝ) → X) (2 * t) else (γ'.extend : (a : ℝ) → X) (2 * t - 1))
      (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) 0 =
    x

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
γ' : Path y z
⊢ Function.comp (α := (↑I : Type))
      (fun (t : ℝ) ↦ if t ≤ 1 / 2 then (γ.extend : (a : ℝ) → X) (2 * t) else (γ'.extend : (a : ℝ) → X) (2 * t - 1))
      (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) 1 =
    z

Tactic:
norm_num
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
pos :
  ∀ (h : (↑t : ℝ) ≤ 1 / 2),
    Eq (α := X) ((γ.extend : (a : ℝ) → X) (2 * (↑t : ℝ)) : X)
      ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯) : X)
neg :
  ∀ (h : ¬(↑t : ℝ) ≤ 1 / 2),
    Eq (α := X) ((γ'.extend : (a : ℝ) → X) (2 * (↑t : ℝ) - 1) : X)
      ((γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯) : X)
⊢ Eq (α := X)
    (if (↑t : ℝ) ≤ 1 / 2 then (γ.extend : (a : ℝ) → X) (2 * (↑t : ℝ))
      else (γ'.extend : (a : ℝ) → X) (2 * (↑t : ℝ) - 1) :
      X)
    (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) ⋯) :
      X)

Tactic:
split_ifs
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
pos :
  Eq (α := X) ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯) : X)
    ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯) : X)
pos₁ : Membership.mem (γ := Set ℝ) (Icc 0 1) (2 * (↑t : ℝ))
pos₂ :
  Eq (α := X) ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯) : X)
    ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯) : X)
pos₃ : Membership.mem (γ := Set ℝ) (Icc 0 1) (2 * (↑t : ℝ))
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) (2 * (↑t : ℝ)) : X)
    ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯) : X)

Tactic:
rw [extend_apply]

Premises used: Path.extend_apply
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
neg :
  Eq (α := X) ((γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯) : X)
    ((γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯) : X)
neg₁ : Membership.mem (γ := Set ℝ) (Icc 0 1) (2 * (↑t : ℝ) - 1)
neg₂ :
  Eq (α := X) ((γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯) : X)
    ((γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯) : X)
neg₃ : Membership.mem (γ := Set ℝ) (Icc 0 1) (2 * (↑t : ℝ) - 1)
⊢ Eq (α := X) ((γ'.extend : (a : ℝ) → X) (2 * (↑t : ℝ) - 1) : X)
    ((γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯) : X)

Tactic:
rw [extend_apply]

Premises used: Path.extend_apply
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
a :
  ∀ (t : (↑I : Type)),
    Eq (α := X) (((γ.trans γ').symm : (a : (↑I : Type)) → X) t : X)
      ((γ'.symm.trans γ.symm : (a : (↑I : Type)) → X) t : X)
⊢ (γ.trans γ').symm = γ'.symm.trans γ.symm

Tactic:
ext t
-- Module: Mathlib.Topology.Path
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : (↑I : Type)
a :
  Eq.{u_1 + 1} (α := X)
    (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
      (γ' : (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) ⋯)))
⊢ Eq (α := X) (((γ.trans γ').symm : (a : (↑I : Type)) → X) t : X) ((γ'.symm.trans γ.symm : (a : (↑I : Type)) → X) t : X)

Tactic:
simp only [trans_apply, symm_apply, Function.comp_apply]

Premises used: Path.symm_apply, Path.trans_apply, Function.comp_apply