awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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 : Fin n → C(X, ℝ)),
    (∀ (i : Fin n), tsupport (α := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ s i) ∧
      EqOn (β := ℝ) (∑ i : Fin n, (⇑(f i) : (a : X) → ℝ)) 1 t ∧
        (∀ (i : Fin n) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)) ∧
          ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑(f i) : (a : X) → ℝ)
have obtain : ∀ (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) → ℝ)),
  ∃ (f : Fin n → C(X, ℝ)),
    (∀ (i : Fin n), tsupport (α := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ s i) ∧
      EqOn (β := ℝ) (∑ i : Fin n, (⇑(f i) : (a : X) → ℝ)) 1 t ∧
        (∀ (i : Fin n) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)) ∧
          ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑(f i) : (a : X) → ℝ)
Tactic: obtain ⟨f, hfsub, hfcp⟩ := PartitionOfUnity.exists_isSubordinate_of_locallyFinite_t2space htcp s
    hs (locallyFinite_of_finite _) hst
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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) → ℝ)
⊢ ∃ (f : Fin n → C(X, ℝ)),
    (∀ (i : Fin n), tsupport (α := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ s i) ∧
      EqOn (β := ℝ) (∑ i : Fin n, (⇑(f i) : (a : X) → ℝ)) 1 t ∧
        (∀ (i : Fin n) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)) ∧
          ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑(f i) : (a : X) → ℝ)
have h : (∀ (i : Fin n), tsupport (α := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) ⊆ s i) ∧
  EqOn (β := ℝ) (∑ i : Fin n, (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) 1 t ∧
    (∀ (i : Fin n) (x : X),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
          ((((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) ∧
      ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
Tactic: use f
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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), tsupport (α := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) ⊆ s i) ∧
    EqOn (β := ℝ) (∑ i : Fin n, (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) 1 t ∧
      (∀ (i : Fin n) (x : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
            ((((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
have h : EqOn (β := ℝ) (∑ i : Fin n, (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) 1 t
Tactic: refine ⟨fun i ↦ hfsub i, ?_, ?_, fun i => hfcp i⟩
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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) → ℝ)
h : EqOn (β := ℝ) (∑ i : Fin n, (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) 1 t
⊢ (∀ (i : Fin n), tsupport (α := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) ⊆ s i) ∧
    EqOn (β := ℝ) (∑ i : Fin n, (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) 1 t ∧
      (∀ (i : Fin n) (x : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
            ((((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
have h₁ : ∀ (i : Fin n) (x : X),
  Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
Tactic: refine ⟨fun i ↦ hfsub i, ?_, ?_, fun i => hfcp i⟩
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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) → ℝ)
x : X
hx : x ∈ t
⊢ Eq (α := ℝ) ((∑ i : Fin n, (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x) (1 x)
have h : Eq (α := ℝ) (∑ c : Fin n, (((f : (a : Fin n) → C(X, ℝ)) c : C(X, ℝ)) : (a : X) → ℝ) x) 1
Tactic: simp only [Finset.sum_apply, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (hypothesis)
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) → ℝ)
x : X
hx : x ∈ t
⊢ Eq (α := ℝ) (∑ c : Fin n, (((f : (a : Fin n) → C(X, ℝ)) c : C(X, ℝ)) : (a : X) → ℝ) x) 1
have h : Eq (α := ℝ) (∑ᶠ (i : Fin n), (f.toFun (s := t) i : (a : X) → ℝ) x) 1
Tactic: have h := f.sum_eq_one' x hx
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (hypothesis)
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) → ℝ)
x : X
hx : x ∈ t
h : Eq (α := ℝ) (∑ᶠ (i : Fin n), (f.toFun (s := t) i : (a : X) → ℝ) x) 1
⊢ Eq (α := ℝ) (∑ c : Fin n, (((f : (a : Fin n) → C(X, ℝ)) c : C(X, ℝ)) : (a : X) → ℝ) x) 1
have h₁ : Eq (α := ℝ)
  (∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : Fin n) ↦ (f.toFun (s := t) i : (a : X) → ℝ) x) sorry,
    (f.toFun (s := t) i : (a : X) → ℝ) x)
  1
Tactic: rw [finsum_eq_sum (fun i => (f.toFun i) x)
      (Finite.subset finite_univ (subset_univ (support fun i ↦ (f.toFun i) x)))] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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) → ℝ)
x : X
hx : x ∈ t
h :
  Eq (α := ℝ)
    (∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : Fin n) ↦ (f.toFun (s := t) i : (a : X) → ℝ) x) ⋯,
      (f.toFun (s := t) i : (a : X) → ℝ) x)
    1
⊢ Eq (α := ℝ) (∑ c : Fin n, (((f : (a : Fin n) → C(X, ℝ)) c : C(X, ℝ)) : (a : X) → ℝ) x) 1
have h₁ : ∀ (h : Eq (α := ℝ) (∑ i : Fin n, (f.toFun (s := t) i : (a : X) → ℝ) x) 1),
  Eq (α := ℝ) (∑ c : Fin n, (((f : (a : Fin n) → C(X, ℝ)) c : C(X, ℝ)) : (a : X) → ℝ) x) 1
Tactic: rwa [Fintype.sum_subset (by simp)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Path (hypothesis)
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)) γ₂)
⊢ γ₁ = γ₂
have h₁ : γ₁.toContinuousMap = γ₂.toContinuousMap
Tactic: simp only [DFunLike.coe_fn_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
γ₁ γ₂ : Path x y
h : γ₁.toContinuousMap = γ₂.toContinuousMap
⊢ γ₁ = γ₂
have 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 γ₁
Cleared hypotheses: γ₁, h
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
γ₂ : 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
⊢ { toContinuousMap := toContinuousMap, source' := source', target' := target' : Path x y } = γ₂
have 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 }
Tactic: cases γ₂
Cleared hypotheses: γ₂, h
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ ofLine ⋯ ⋯ ⋯ = γ
have a : ∀ (t : (↑I : Type)), Eq (α := X) ((ofLine sorry sorry sorry : (a : (↑I : Type)) → X) t : X) ((γ : (a : (↑I : Type)) → X) t : X)
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
ι : Type u_3
γ_1 γ : Path x y
γ' : Path y z
⊢ 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))
have refine_1 : Continuous[_, inst] fun (t : ℝ) ↦ (γ.extend : (a : ℝ) → X) (2 * t)
Tactic: refine
      (Continuous.if_le ?_ ?_ continuous_id continuous_const (by simp)).comp
        continuous_subtype_val
-- Lean 4 proof step from Mathlib.Topology.Path (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
γ_1 γ : Path x y
γ' : Path y z
refine_1 : Continuous[_, inst] fun (t : ℝ) ↦ (γ.extend : (a : ℝ) → X) (2 * t)
⊢ 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))
have refine_2 : Continuous[_, inst] fun (t : ℝ) ↦ (γ'.extend : (a : ℝ) → X) (2 * t - 1)
Tactic: refine
      (Continuous.if_le ?_ ?_ continuous_id continuous_const (by simp)).comp
        continuous_subtype_val
-- 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 : (↑I : Type)
⊢ 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)
have 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 : ℝ)) sorry) : X)
Tactic: split_ifs
-- 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 : (↑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)
⊢ 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)
have 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) sorry) : X)
Tactic: split_ifs
-- 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 : (↑I : Type)
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)
have pos : Eq (α := X) ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) sorry) : X)
  ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) sorry) : X)
Tactic: rw [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 : (↑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)
⊢ Eq (α := X) ((γ.extend : (a : ℝ) → X) (2 * (↑t : ℝ)) : X)
    ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯) : X)
have pos₁ : Membership.mem (γ := Set ℝ) (Icc 0 1) (2 * (↑t : ℝ))
Tactic: rw [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 : (↑I : Type)
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)
have neg : Eq (α := X) ((γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) sorry) : X)
  ((γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) sorry) : X)
Tactic: rw [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 : (↑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)
⊢ Eq (α := X) ((γ'.extend : (a : ℝ) → X) (2 * (↑t : ℝ) - 1) : X)
    ((γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) ⋯) : X)
have neg₁ : Membership.mem (γ := Set ℝ) (Icc 0 1) (2 * (↑t : ℝ) - 1)
Tactic: rw [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
⊢ (γ.trans γ').symm = γ'.symm.trans γ.symm
have a : ∀ (t : (↑I : Type)),
  Eq (α := X) (((γ.trans γ').symm : (a : (↑I : Type)) → X) t : X) ((γ'.symm.trans γ.symm : (a : (↑I : Type)) → X) t : X)
Tactic: ext 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 : (↑I : Type)
⊢ Eq (α := X) (((γ.trans γ').symm : (a : (↑I : Type)) → X) t : X) ((γ'.symm.trans γ.symm : (a : (↑I : Type)) → X) t : X)
have 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) : ℝ)) sorry)
  else (γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ) - 1) sorry))
  (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)))
Tactic: simp only [trans_apply, symm_apply, Function.comp_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 : (↑I : Type)
⊢ 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) ⋯)))
have pos : ∀ (h : (↑(σ t) : ℝ) ≤ 1 / 2) (h₁ : (↑t : ℝ) ≤ 1 / 2),
  Eq (α := X) ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ)) sorry) : X)
    ((γ' : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) sorry)) : X)
Tactic: split_ifs with h h₁ h₂
-- 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 : (↑I : Type)
pos :
  ∀ (h : (↑(σ t) : ℝ) ≤ 1 / 2) (h₁ : (↑t : ℝ) ≤ 1 / 2),
    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)
⊢ 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) ⋯)))
have neg : ∀ (h : (↑(σ t) : ℝ) ≤ 1 / 2) (h₁ : ¬(↑t : ℝ) ≤ 1 / 2),
  Eq (α := X) ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ)) sorry) : X)
    ((γ : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) sorry)) : X)
Tactic: split_ifs with h h₁ h₂
-- 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 : (↑I : Type)
pos :
  ∀ (h : (↑(σ t) : ℝ) ≤ 1 / 2) (h₁ : (↑t : ℝ) ≤ 1 / 2),
    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)
neg :
  ∀ (h : (↑(σ t) : ℝ) ≤ 1 / 2) (h₁ : ¬(↑t : ℝ) ≤ 1 / 2),
    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 : ℝ) - 1) ⋯)) : X)
⊢ 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) ⋯)))
have pos₁ : ∀ (h : ¬(↑(σ t) : ℝ) ≤ 1 / 2) (h₂ : (↑t : ℝ) ≤ 1 / 2),
  Eq (α := X) ((γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ) - 1) sorry) : X)
    ((γ' : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) sorry)) : X)
Tactic: split_ifs with h h₁ h₂
-- 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 : (↑I : Type)
pos :
  ∀ (h : (↑(σ t) : ℝ) ≤ 1 / 2) (h₁ : (↑t : ℝ) ≤ 1 / 2),
    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)
neg :
  ∀ (h : (↑(σ t) : ℝ) ≤ 1 / 2) (h₁ : ¬(↑t : ℝ) ≤ 1 / 2),
    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 : ℝ) - 1) ⋯)) : X)
pos₁ :
  ∀ (h : ¬(↑(σ t) : ℝ) ≤ 1 / 2) (h₂ : (↑t : ℝ) ≤ 1 / 2),
    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 : ℝ)) ⋯)) : X)
⊢ 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) ⋯)))
have neg₁ : ∀ (h : ¬(↑(σ t) : ℝ) ≤ 1 / 2) (h₂ : ¬(↑t : ℝ) ≤ 1 / 2),
  Eq (α := X) ((γ' : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ) - 1) sorry) : X)
    ((γ : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ) - 1) sorry)) : X)
Tactic: split_ifs with h h₁ h₂
-- 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 : (↑I : Type)
h : (↑(σ t) : ℝ) ≤ 1 / 2
h₁ : (↑t : ℝ) ≤ 1 / 2
⊢ 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)
have pos : ∀ (h_1 : 1 - (↑t : ℝ) ≤ 1 / 2) (h₁ : (↑t : ℝ) ≤ 1 / 2),
  Eq (α := X) ((γ : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑(σ t) : ℝ)) sorry) : X)
    ((γ' : (a : (↑I : Type)) → X) (σ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) sorry)) : X)
Tactic: rw [coe_symm_eq] at h
Cleared hypotheses: h₁