awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ :
  ∀ a ∈ U₁,
    ∃ (t : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} t ∧ a ∈ t ∧ t ⊆ U₁
hU₂ :
  ∀ a ∈ U₂,
    ∃ (t : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} t ∧ a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
W₁ : Set X
hW₁ : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} W₁ ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁
W₂ : Set X
hW₂ : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} W₂ ∧ x₂ ∈ W₂ ∧ W₂ ⊆ U₂
z : X
hz : z ∈ Z
hc : z ∉ W₁ᶜ ∪ W₂ᶜ
⊢ False
have hc₁ : z ∈ W₁ ∧ z ∈ W₂
Tactic: simp only [Set.mem_union, Set.mem_compl_iff, not_or, not_not] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : (↑I : Type)
⊢ (γ.subpath t₀ t₁).symm = γ.subpath t₁ t₀
have a₁ : ∀ (s : (↑I : Type)),
  Eq (α := X) (((γ.subpath t₀ t₁).symm : (a : (↑I : Type)) → X) s : X) ((γ.subpath t₁ t₀ : (a : (↑I : Type)) → X) s : X)
Tactic: ext s
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
t₀ t₁ : (↑I : Type)
⊢ range (Icc.convexComb t₀ t₁) = uIcc t₀ t₁
have rw : (∀ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a ∈ uIcc t₀ t₁) ∧
  ∀ b ∈ uIcc t₀ t₁, ∃ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a = b
Tactic: rw [range_eq_iff]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
t₀ t₁ : (↑I : Type)
⊢ (∀ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a ∈ uIcc t₀ t₁) ∧
    ∀ b ∈ uIcc t₀ t₁, ∃ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a = b
have left : ∀ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a ∈ uIcc t₀ t₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
t₀ t₁ : (↑I : Type)
left : ∀ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a ∈ uIcc t₀ t₁
⊢ (∀ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a ∈ uIcc t₀ t₁) ∧
    ∀ b ∈ uIcc t₀ t₁, ∃ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a = b
have right : ∀ b ∈ uIcc t₀ t₁, ∃ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
t₀ t₁ : (↑I : Type)
t : (↑(Icc 0 1) : Type)
⊢ t ∈ uIcc t₀ t₁ → ∃ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a = t
have right : ∀ (ht : (↑t : ℝ) ∈ uIcc (↑t₀ : ℝ) (↑t₁ : ℝ)), ∃ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a = t
Tactic: (ht : (t : ℝ) ∈ uIcc (t₀ : ℝ) (t₁ : ℝ))
-- Lean 4 proof step from Mathlib.Topology.Subpath (hypothesis)
Goal:
t₀ t₁ : (↑I : Type)
t : (↑(Icc 0 1) : Type)
ht : (↑t : ℝ) ∈ uIcc (↑t₀ : ℝ) (↑t₁ : ℝ)
⊢ ∃ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a = t
have ht₁ : Membership.mem (γ := Set ℝ) ((fun (θ : ℝ) ↦ (1 - θ) • (↑t₀ : ℝ) + θ • (↑t₁ : ℝ)) '' Icc 0 1) (↑t : ℝ)
Tactic: rw [← segment_eq_uIcc, segment_eq_image] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
t₀ t₁ : (↑I : Type)
t : (↑(Icc 0 1) : Type)
ht : Membership.mem (γ := Set ℝ) ((fun (θ : ℝ) ↦ (1 - θ) • (↑t₀ : ℝ) + θ • (↑t₁ : ℝ)) '' Icc 0 1) (↑t : ℝ)
⊢ ∃ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a = t
have right : ∀ (s : ℝ) (hs : Membership.mem (γ := Set ℝ) (Icc 0 1) s)
  (hst : (fun (θ : ℝ) ↦ (1 - θ) • (↑t₀ : ℝ) + θ • (↑t₁ : ℝ)) s = (↑t : ℝ)),
  ∃ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a = t
Tactic: obtain ⟨s, hs, hst⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
t₀ t₁ : (↑I : Type)
t : (↑(Icc 0 1) : Type)
s : ℝ
hs : Membership.mem (γ := Set ℝ) (Icc 0 1) s
hst : (fun (θ : ℝ) ↦ (1 - θ) • (↑t₀ : ℝ) + θ • (↑t₁ : ℝ)) s = (↑t : ℝ)
⊢ ∃ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a = t
have h : Icc.convexComb t₀ t₁ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) s hs) = t
Tactic: use ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
t₀ t₁ : (↑I : Type)
t : (↑(Icc 0 1) : Type)
s : ℝ
hs : Membership.mem (γ := Set ℝ) (Icc 0 1) s
hst : (fun (θ : ℝ) ↦ (1 - θ) • (↑t₀ : ℝ) + θ • (↑t₁ : ℝ)) s = (↑t : ℝ)
⊢ Icc.convexComb t₀ t₁ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) s hs) = t
have h : (↑(Icc.convexComb t₀ t₁ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) s hs)) : ℝ) = (↑t : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : (↑I : Type)
⊢ Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.subpath t₀ t₁) : (a : (↑I : Type)) → X))
    ((⇑γ : (a : (↑I : Type)) → X) '' uIcc t₀ t₁)
have rw : Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.subpath t₀ t₁) : (a : (↑I : Type)) → X))
  ((⇑γ : (a : (↑I : Type)) → X) '' range (Icc.convexComb t₀ t₁))
Tactic: rw [← range_subpathAux, ← range_comp, subpath, coe_mk', ContinuousMap.coe_mk]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : (↑I : Type)
rw :
  Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.subpath t₀ t₁) : (a : (↑I : Type)) → X))
    ((⇑γ : (a : (↑I : Type)) → X) '' range (Icc.convexComb t₀ t₁))
⊢ Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.subpath t₀ t₁) : (a : (↑I : Type)) → X))
    ((⇑γ : (a : (↑I : Type)) → X) '' uIcc t₀ t₁)
have rw₁ : Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.subpath t₀ t₁) : (a : (↑I : Type)) → X))
  (range ((⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁))
Tactic: rw [← range_subpathAux, ← range_comp, subpath, coe_mk', ContinuousMap.coe_mk]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : (↑I : Type)
rw :
  Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.subpath t₀ t₁) : (a : (↑I : Type)) → X))
    ((⇑γ : (a : (↑I : Type)) → X) '' range (Icc.convexComb t₀ t₁))
rw₁ :
  Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.subpath t₀ t₁) : (a : (↑I : Type)) → X))
    (range ((⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁))
⊢ Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.subpath t₀ t₁) : (a : (↑I : Type)) → X))
    ((⇑γ : (a : (↑I : Type)) → X) '' uIcc t₀ t₁)
have rw₂ : Eq (α := Set X)
  (range (ι := (↑I : Type))
    (⇑{ toFun := (⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁, continuous_toFun := sorry, source' := sorry,
          target' := sorry : Path (X := X) ((γ : (a : (↑I : Type)) → X) t₀ : X) ((γ : (a : (↑I : Type)) → X) t₁ : X) } :
      (a : (↑I : Type)) → X))
  (range ((⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁))
Tactic: rw [← range_subpathAux, ← range_comp, subpath, coe_mk', ContinuousMap.coe_mk]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : (↑I : Type)
rw :
  Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.subpath t₀ t₁) : (a : (↑I : Type)) → X))
    ((⇑γ : (a : (↑I : Type)) → X) '' range (Icc.convexComb t₀ t₁))
rw₁ :
  Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.subpath t₀ t₁) : (a : (↑I : Type)) → X))
    (range ((⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁))
rw₂ :
  Eq (α := Set X)
    (range (ι := (↑I : Type))
      (⇑{ toFun := (⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁, continuous_toFun := ⋯, source' := ⋯,
            target' := ⋯ : Path (X := X) ((γ : (a : (↑I : Type)) → X) t₀ : X) ((γ : (a : (↑I : Type)) → X) t₁ : X) } :
        (a : (↑I : Type)) → X))
    (range ((⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁))
⊢ Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.subpath t₀ t₁) : (a : (↑I : Type)) → X))
    ((⇑γ : (a : (↑I : Type)) → X) '' uIcc t₀ t₁)
have rw₃ : Eq (α := Set X)
  (range (ι := (↑I : Type))
    (⇑{ toFun := (⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁, continuous_toFun := sorry : C((↑I : Type), X) } :
      (a : (↑I : Type)) → X))
  (range ((⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁))
Tactic: rw [← range_subpathAux, ← range_comp, subpath, coe_mk', ContinuousMap.coe_mk]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : (↑I : Type)
rw :
  Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.subpath t₀ t₁) : (a : (↑I : Type)) → X))
    ((⇑γ : (a : (↑I : Type)) → X) '' range (Icc.convexComb t₀ t₁))
rw₁ :
  Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.subpath t₀ t₁) : (a : (↑I : Type)) → X))
    (range ((⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁))
rw₂ :
  Eq (α := Set X)
    (range (ι := (↑I : Type))
      (⇑{ toFun := (⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁, continuous_toFun := ⋯, source' := ⋯,
            target' := ⋯ : Path (X := X) ((γ : (a : (↑I : Type)) → X) t₀ : X) ((γ : (a : (↑I : Type)) → X) t₁ : X) } :
        (a : (↑I : Type)) → X))
    (range ((⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁))
rw₃ :
  Eq (α := Set X)
    (range (ι := (↑I : Type))
      (⇑{ toFun := (⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁, continuous_toFun := ⋯ : C((↑I : Type), X) } :
        (a : (↑I : Type)) → X))
    (range ((⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁))
⊢ Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.subpath t₀ t₁) : (a : (↑I : Type)) → X))
    ((⇑γ : (a : (↑I : Type)) → X) '' uIcc t₀ t₁)
have rw₄ : Eq (α := Set X) (range ((⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁))
  (range ((⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁))
Tactic: rw [← range_subpathAux, ← range_comp, subpath, coe_mk', ContinuousMap.coe_mk]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t : (↑I : Type)
⊢ γ.subpath t t = refl ((γ : (a : (↑I : Type)) → X) t)
have a₁ : ∀ (s : (↑I : Type)),
  Eq (α := X) ((γ.subpath t t : (a : (↑I : Type)) → X) s : X)
    (((refl ((γ : (a : (↑I : Type)) → X) t) :
            Path (X := X) ((γ : (a : (↑I : Type)) → X) t : X) ((γ : (a : (↑I : Type)) → X) t : X)) :
          (a : (↑I : Type)) → X)
        s :
      X)
Tactic: ext s
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
⊢ γ.subpath 0 1 = γ.cast ⋯ ⋯
have a₁ : ∀ (s : (↑I : Type)),
  Eq (α := X) ((γ.subpath 0 1 : (a : (↑I : Type)) → X) s : X) ((γ.cast sorry sorry : (a : (↑I : Type)) → X) s : X)
Tactic: ext s
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : (↑I : Type)
γ₁ : (t : (↑I : Type)) →
  Path (X := X) ((γ : (a : (↑I : Type)) → X) t₀ : X) ((γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ t) : X) :=
  fun (t : (↑I : Type)) ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : (↑I : Type)) →
  Path (X := X) ((γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ t) : X) ((γ : (a : (↑I : Type)) → X) t₂ : X) :=
  fun (t : (↑I : Type)) ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
⊢ Continuous.{0, u_1} (Y := X) fun (x : (↑I : Type) × (↑I : Type)) ↦
    (Path.trans (y := (γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ x.1)) (γ.subpath t₀ (Icc.convexComb t₁ t₂ x.1))
          (γ.subpath (Icc.convexComb t₁ t₂ x.1) t₂) :
        (a : (↑I : Type)) → X)
      x.2
have refine_1 : Continuous ↿γ₁
Tactic: refine Path.trans_continuous_family γ₁ ?_ γ₂ ?_
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : (↑I : Type)
γ₁ : (t : (↑I : Type)) →
  Path (X := X) ((γ : (a : (↑I : Type)) → X) t₀ : X) ((γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ t) : X) :=
  fun (t : (↑I : Type)) ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : (↑I : Type)) →
  Path (X := X) ((γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ t) : X) ((γ : (a : (↑I : Type)) → X) t₂ : X) :=
  fun (t : (↑I : Type)) ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
refine_1 : Continuous ↿γ₁
⊢ Continuous.{0, u_1} (Y := X) fun (x : (↑I : Type) × (↑I : Type)) ↦
    (Path.trans (y := (γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ x.1)) (γ.subpath t₀ (Icc.convexComb t₁ t₂ x.1))
          (γ.subpath (Icc.convexComb t₁ t₂ x.1) t₂) :
        (a : (↑I : Type)) → X)
      x.2
have refine_2 : Continuous ↿γ₂
Tactic: refine Path.trans_continuous_family γ₁ ?_ γ₂ ?_
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : (↑I : Type)
γ₁ : (t : (↑I : Type)) →
  Path (X := X) ((γ : (a : (↑I : Type)) → X) t₀ : X) ((γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ t) : X) :=
  fun (t : (↑I : Type)) ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : (↑I : Type)) →
  Path (X := X) ((γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ t) : X) ((γ : (a : (↑I : Type)) → X) t₂ : X) :=
  fun (t : (↑I : Type)) ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
⊢ Continuous ↿γ₁
have refine_1 : Continuous (Y := (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦ t₀
Tactic: refine γ.subpath_continuous_family.comp (.prodMk ?_ <| .prodMk ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : (↑I : Type)
γ₁ : (t : (↑I : Type)) →
  Path (X := X) ((γ : (a : (↑I : Type)) → X) t₀ : X) ((γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ t) : X) :=
  fun (t : (↑I : Type)) ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : (↑I : Type)) →
  Path (X := X) ((γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ t) : X) ((γ : (a : (↑I : Type)) → X) t₂ : X) :=
  fun (t : (↑I : Type)) ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
refine_1 : Continuous (Y := (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦ t₀
⊢ Continuous ↿γ₁
have refine_1₁ : Continuous (Y := (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦
  Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) x)
    ((1 - (↑x.1 : ℝ)) * (↑t₁ : ℝ) + (↑x.1 : ℝ) * (↑t₂ : ℝ)) sorry
Tactic: refine γ.subpath_continuous_family.comp (.prodMk ?_ <| .prodMk ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : (↑I : Type)
γ₁ : (t : (↑I : Type)) →
  Path (X := X) ((γ : (a : (↑I : Type)) → X) t₀ : X) ((γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ t) : X) :=
  fun (t : (↑I : Type)) ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : (↑I : Type)) →
  Path (X := X) ((γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ t) : X) ((γ : (a : (↑I : Type)) → X) t₂ : X) :=
  fun (t : (↑I : Type)) ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
refine_1 : Continuous (Y := (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦ t₀
refine_1₁ :
  Continuous (Y := (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦
    Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) x)
      ((1 - (↑x.1 : ℝ)) * (↑t₁ : ℝ) + (↑x.1 : ℝ) * (↑t₂ : ℝ)) ⋯
⊢ Continuous ↿γ₁
have refine_1₂ : Continuous (Y := (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦ x.2
Tactic: refine γ.subpath_continuous_family.comp (.prodMk ?_ <| .prodMk ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : (↑I : Type)
γ₁ : (t : (↑I : Type)) →
  Path (X := X) ((γ : (a : (↑I : Type)) → X) t₀ : X) ((γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ t) : X) :=
  fun (t : (↑I : Type)) ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : (↑I : Type)) →
  Path (X := X) ((γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ t) : X) ((γ : (a : (↑I : Type)) → X) t₂ : X) :=
  fun (t : (↑I : Type)) ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
⊢ Continuous ↿γ₂
have refine_2 : Continuous (Y := (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦
  Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) x)
    ((1 - (↑x.1 : ℝ)) * (↑t₁ : ℝ) + (↑x.1 : ℝ) * (↑t₂ : ℝ)) sorry
Tactic: refine γ.subpath_continuous_family.comp (.prodMk ?_ <| .prodMk ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : (↑I : Type)
γ₁ : (t : (↑I : Type)) →
  Path (X := X) ((γ : (a : (↑I : Type)) → X) t₀ : X) ((γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ t) : X) :=
  fun (t : (↑I : Type)) ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : (↑I : Type)) →
  Path (X := X) ((γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ t) : X) ((γ : (a : (↑I : Type)) → X) t₂ : X) :=
  fun (t : (↑I : Type)) ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
refine_2 :
  Continuous (Y := (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦
    Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) x)
      ((1 - (↑x.1 : ℝ)) * (↑t₁ : ℝ) + (↑x.1 : ℝ) * (↑t₂ : ℝ)) ⋯
⊢ Continuous ↿γ₂
have refine_2₁ : Continuous (Y := (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦ t₂
Tactic: refine γ.subpath_continuous_family.comp (.prodMk ?_ <| .prodMk ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : (↑I : Type)
γ₁ : (t : (↑I : Type)) →
  Path (X := X) ((γ : (a : (↑I : Type)) → X) t₀ : X) ((γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ t) : X) :=
  fun (t : (↑I : Type)) ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : (↑I : Type)) →
  Path (X := X) ((γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ t) : X) ((γ : (a : (↑I : Type)) → X) t₂ : X) :=
  fun (t : (↑I : Type)) ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
refine_2 :
  Continuous (Y := (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦
    Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) x)
      ((1 - (↑x.1 : ℝ)) * (↑t₁ : ℝ) + (↑x.1 : ℝ) * (↑t₂ : ℝ)) ⋯
refine_2₁ : Continuous (Y := (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦ t₂
⊢ Continuous ↿γ₂
have refine_2₂ : Continuous (Y := (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦ x.2
Tactic: refine γ.subpath_continuous_family.comp (.prodMk ?_ <| .prodMk ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ x : (↑I : Type)
⊢ Eq (α := X)
    ((Path.trans (y := (γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ (0, x).1))
            (γ.subpath t₀ (Icc.convexComb t₁ t₂ (0, x).1)) (γ.subpath (Icc.convexComb t₁ t₂ (0, x).1) t₂) :
          (a : (↑I : Type)) → X)
        (0, x).2 :
      X)
    ((((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂)).toContinuousMap : (a : (↑I : Type)) → X) x : X)
have rw : Eq (α := X) (((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂) : (a : (↑I : Type)) → X) (0, x).2 : X)
  ((((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂)).toContinuousMap : (a : (↑I : Type)) → X) x : X)
Tactic: rw [Icc.convexComb_zero, coe_toContinuousMap]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ x : (↑I : Type)
rw :
  Eq (α := X) (((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂) : (a : (↑I : Type)) → X) (0, x).2 : X)
    ((((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂)).toContinuousMap : (a : (↑I : Type)) → X) x : X)
⊢ Eq (α := X)
    ((Path.trans (y := (γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ (0, x).1))
            (γ.subpath t₀ (Icc.convexComb t₁ t₂ (0, x).1)) (γ.subpath (Icc.convexComb t₁ t₂ (0, x).1) t₂) :
          (a : (↑I : Type)) → X)
        (0, x).2 :
      X)
    ((((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂)).toContinuousMap : (a : (↑I : Type)) → X) x : X)
have rw₁ : Eq (α := X) (((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂) : (a : (↑I : Type)) → X) (0, x).2 : X)
  (((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂) : (a : (↑I : Type)) → X) x : X)
Tactic: rw [Icc.convexComb_zero, coe_toContinuousMap]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ x : (↑I : Type)
⊢ Eq (α := X)
    ((Path.trans (y := (γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ (1, x).1))
            (γ.subpath t₀ (Icc.convexComb t₁ t₂ (1, x).1)) (γ.subpath (Icc.convexComb t₁ t₂ (1, x).1) t₂) :
          (a : (↑I : Type)) → X)
        (1, x).2 :
      X)
    ((toContinuousMap (y := (γ : (a : (↑I : Type)) → X) t₂)
            ((γ.subpath t₀ t₂).trans (Path.refl ((γ : (a : (↑I : Type)) → X) t₂))) :
          (a : (↑I : Type)) → X)
        x :
      X)
have rw : Eq (α := X) (((γ.subpath t₀ t₂).trans (γ.subpath t₂ t₂) : (a : (↑I : Type)) → X) (1, x).2 : X)
  ((toContinuousMap (y := (γ : (a : (↑I : Type)) → X) t₂)
          ((γ.subpath t₀ t₂).trans (Path.refl ((γ : (a : (↑I : Type)) → X) t₂))) :
        (a : (↑I : Type)) → X)
      x :
    X)
Tactic: rw [Icc.convexComb_one, subpath_self, coe_toContinuousMap]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ x : (↑I : Type)
rw :
  Eq (α := X) (((γ.subpath t₀ t₂).trans (γ.subpath t₂ t₂) : (a : (↑I : Type)) → X) (1, x).2 : X)
    ((toContinuousMap (y := (γ : (a : (↑I : Type)) → X) t₂)
            ((γ.subpath t₀ t₂).trans (Path.refl ((γ : (a : (↑I : Type)) → X) t₂))) :
          (a : (↑I : Type)) → X)
        x :
      X)
⊢ Eq (α := X)
    ((Path.trans (y := (γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ (1, x).1))
            (γ.subpath t₀ (Icc.convexComb t₁ t₂ (1, x).1)) (γ.subpath (Icc.convexComb t₁ t₂ (1, x).1) t₂) :
          (a : (↑I : Type)) → X)
        (1, x).2 :
      X)
    ((toContinuousMap (y := (γ : (a : (↑I : Type)) → X) t₂)
            ((γ.subpath t₀ t₂).trans (Path.refl ((γ : (a : (↑I : Type)) → X) t₂))) :
          (a : (↑I : Type)) → X)
        x :
      X)
have rw₁ : Eq (α := X)
  (((γ.subpath t₀ t₂).trans (Path.refl ((γ : (a : (↑I : Type)) → X) t₂)) : (a : (↑I : Type)) → X) (1, x).2 : X)
  ((toContinuousMap (y := (γ : (a : (↑I : Type)) → X) t₂)
          ((γ.subpath t₀ t₂).trans (Path.refl ((γ : (a : (↑I : Type)) → X) t₂))) :
        (a : (↑I : Type)) → X)
      x :
    X)
Tactic: rw [Icc.convexComb_one, subpath_self, coe_toContinuousMap]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ x : (↑I : Type)
rw :
  Eq (α := X) (((γ.subpath t₀ t₂).trans (γ.subpath t₂ t₂) : (a : (↑I : Type)) → X) (1, x).2 : X)
    ((toContinuousMap (y := (γ : (a : (↑I : Type)) → X) t₂)
            ((γ.subpath t₀ t₂).trans (Path.refl ((γ : (a : (↑I : Type)) → X) t₂))) :
          (a : (↑I : Type)) → X)
        x :
      X)
rw₁ :
  Eq (α := X)
    (((γ.subpath t₀ t₂).trans (Path.refl ((γ : (a : (↑I : Type)) → X) t₂)) : (a : (↑I : Type)) → X) (1, x).2 : X)
    ((toContinuousMap (y := (γ : (a : (↑I : Type)) → X) t₂)
            ((γ.subpath t₀ t₂).trans (Path.refl ((γ : (a : (↑I : Type)) → X) t₂))) :
          (a : (↑I : Type)) → X)
        x :
      X)
⊢ Eq (α := X)
    ((Path.trans (y := (γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ (1, x).1))
            (γ.subpath t₀ (Icc.convexComb t₁ t₂ (1, x).1)) (γ.subpath (Icc.convexComb t₁ t₂ (1, x).1) t₂) :
          (a : (↑I : Type)) → X)
        (1, x).2 :
      X)
    ((toContinuousMap (y := (γ : (a : (↑I : Type)) → X) t₂)
            ((γ.subpath t₀ t₂).trans (Path.refl ((γ : (a : (↑I : Type)) → X) t₂))) :
          (a : (↑I : Type)) → X)
        x :
      X)
have rw₂ : Eq (α := X)
  (((γ.subpath t₀ t₂).trans (Path.refl ((γ : (a : (↑I : Type)) → X) t₂)) : (a : (↑I : Type)) → X) (1, x).2 : X)
  (((γ.subpath t₀ t₂).trans (Path.refl ((γ : (a : (↑I : Type)) → X) t₂)) : (a : (↑I : Type)) → X) x : X)
Tactic: rw [Icc.convexComb_one, subpath_self, coe_toContinuousMap]