awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Spectral.Prespectral
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₂
⊢ x₂ ∈ Z ∩ W₂ᶜᶜ

Tactic:
grind
-- Module: Mathlib.Topology.Spectral.Prespectral
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₂
refine : ∀ (z : X) (hz : z ∈ Z), z ∈ W₁ᶜ ∪ W₂ᶜ
⊢ ∃ (A : Set X) (B : Set X),
    IsClosed[inst] A ∧
      IsClosed[inst] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty

Tactic:
refine ⟨W₁ᶜ, W₂ᶜ, by simpa using hW₁.1.1, by simpa using hW₂.1.1, by simp [hW₁.1.2],
    by simp [hW₂.1.2], fun z hz ↦ ?_, ⟨x₁, by grind⟩, ⟨x₂, by grind⟩⟩
-- Module: Mathlib.Topology.Spectral.Prespectral
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
by_contra! : ∀ (hc : z ∉ W₁ᶜ ∪ W₂ᶜ), False
⊢ z ∈ W₁ᶜ ∪ W₂ᶜ

Tactic:
by_contra! hc
-- Module: Mathlib.Topology.Spectral.Prespectral
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₂ᶜ
⊢ z ∈ W₁ ∧ z ∈ W₂

Tactic:
simp only [Set.mem_union, Set.mem_compl_iff, not_or, not_not] at hc

Premises used: Set.mem_union, Classical.not_not, not_or, Set.mem_compl_iff
-- Module: Mathlib.Topology.Spectral.Prespectral
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₁ ∧ z ∈ W₂
⊢ False

Tactic:
hU₁₂ ⟨hz, hW₁.2.2 hc.1, hW₂.2.2 hc.2⟩

Premises used: Set.Mem, And.right, And.left, And.intro
-- Module: Mathlib.Topology.Spectral.Prespectral
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₁ ∧ z ∈ W₂
⊢ False

Tactic:
exact hU₁₂ ⟨hz, hW₁.2.2 hc.1, hW₂.2.2 hc.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : (↑I : Type)
⊢ Eq (α := X) (((⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁) 0 : X) ((γ : (a : (↑I : Type)) → X) t₀ : X)

Tactic:
simp
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : (↑I : Type)
⊢ Eq (α := X) (((⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁) 1 : X) ((γ : (a : (↑I : Type)) → X) t₁ : X)

Tactic:
simp
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : (↑I : Type)
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)
⊢ (γ.subpath t₀ t₁).symm = γ.subpath t₁ t₀

Tactic:
ext s
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ 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:
simp [subpath]

Premises used: Path.subpath
-- Module: Mathlib.Topology.Subpath
Goal:
t₀ t₁ : (↑I : Type)
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
⊢ range (Icc.convexComb t₀ t₁) = uIcc t₀ t₁

Tactic:
rw [range_eq_iff]

Premises used: Set.range_eq_iff
-- Module: Mathlib.Topology.Subpath
Goal:
t₀ t₁ : (↑I : Type)
left : ∀ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a ∈ uIcc t₀ t₁
right : ∀ b ∈ uIcc t₀ t₁, ∃ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a = b
⊢ (∀ (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:
constructor
-- Module: Mathlib.Topology.Subpath
Goal:
t₀ t₁ s : (↑I : Type)
⊢ Icc.convexComb t₀ t₁ s ∈ uIcc t₀ t₁

Tactic:
convex_uIcc (t₀ : ℝ) t₁ left_mem_uIcc right_mem_uIcc
      (one_minus_nonneg s) (nonneg s) (sub_add_cancel _ _)

Premises used: Set.Mem, setOf, Set.right_mem_uIcc, Set.left_mem_uIcc, convex_uIcc, Set.Icc, unitInterval.nonneg, unitInterval.one_minus_nonneg, Subtype.val, sub_add_cancel, Set.uIcc
-- Module: Mathlib.Topology.Subpath
Goal:
t₀ t₁ s : (↑I : Type)
⊢ Icc.convexComb t₀ t₁ s ∈ uIcc t₀ t₁

Tactic:
exact convex_uIcc (t₀ : ℝ) t₁ left_mem_uIcc right_mem_uIcc
      (one_minus_nonneg s) (nonneg s) (sub_add_cancel _ _)

Premises used: Set.right_mem_uIcc, Set.left_mem_uIcc, convex_uIcc, unitInterval.nonneg, unitInterval.one_minus_nonneg, Subtype.val, sub_add_cancel
-- Module: Mathlib.Topology.Subpath
Goal:
t₀ t₁ : (↑I : Type)
t : (↑(Icc 0 1) : Type)
right : ∀ (ht : (↑t : ℝ) ∈ uIcc (↑t₀ : ℝ) (↑t₁ : ℝ)), ∃ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a = t
⊢ t ∈ uIcc t₀ t₁ → ∃ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a = t

Tactic:
(ht : (t : ℝ) ∈ uIcc (t₀ : ℝ) (t₁ : ℝ))
-- Module: Mathlib.Topology.Subpath
Goal:
t₀ t₁ : (↑I : Type)
t : (↑(Icc 0 1) : Type)
ht : (↑t : ℝ) ∈ uIcc (↑t₀ : ℝ) (↑t₁ : ℝ)
⊢ Membership.mem (γ := Set ℝ) ((fun (θ : ℝ) ↦ (1 - θ) • (↑t₀ : ℝ) + θ • (↑t₁ : ℝ)) '' Icc 0 1) (↑t : ℝ)

Tactic:
rw [← segment_eq_uIcc, segment_eq_image] at ht

Premises used: segment_eq_uIcc, segment_eq_image
-- Module: Mathlib.Topology.Subpath
Goal:
t₀ t₁ : (↑I : Type)
t : (↑(Icc 0 1) : Type)
ht : Membership.mem (γ := Set ℝ) ((fun (θ : ℝ) ↦ (1 - θ) • (↑t₀ : ℝ) + θ • (↑t₁ : ℝ)) '' Icc 0 1) (↑t : ℝ)
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
⊢ ∃ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a = t

Tactic:
obtain ⟨s, hs, hst⟩ := ht
-- Module: Mathlib.Topology.Subpath
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 : ℝ)
h : Icc.convexComb t₀ t₁ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) s hs) = t
⊢ ∃ (a : (↑I : Type)), Icc.convexComb t₀ t₁ a = t

Tactic:
use ⟨s, hs⟩
-- Module: Mathlib.Topology.Subpath
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 : ℝ)
h : (↑(Icc.convexComb t₀ t₁ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) s hs)) : ℝ) = (↑t : ℝ)
⊢ Icc.convexComb t₀ t₁ (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) s hs) = t

Tactic:
ext
-- Module: Mathlib.Topology.Subpath
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 : ℝ)

Tactic:
hst
-- Module: Mathlib.Topology.Subpath
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 : ℝ)

Tactic:
exact hst
-- Module: Mathlib.Topology.Subpath
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₁))
rw₄ rw₅ :
  Eq (α := Set X) (range ((⇑γ : (a : (↑I : Type)) → X) ∘ Icc.convexComb t₀ t₁))
    (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₁)

Tactic:
rw [← range_subpathAux, ← range_comp, subpath, coe_mk', ContinuousMap.coe_mk]

Premises used: Set.range_comp, Path.range_subpathAux, ContinuousMap.coe_mk, Path.coe_mk', Path.subpath
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : (↑I : Type)
h : t₀ ≤ t₁
⊢ Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.subpath t₀ t₁) : (a : (↑I : Type)) → X))
    ((⇑γ : (a : (↑I : Type)) → X) '' Icc t₀ t₁)

Tactic:
simp [h]
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : (↑I : Type)
h : t₁ ≤ t₀
⊢ Eq (α := Set X) (range (ι := (↑I : Type)) (⇑(γ.subpath t₀ t₁) : (a : (↑I : Type)) → X))
    ((⇑γ : (a : (↑I : Type)) → X) '' Icc t₁ t₀)

Tactic:
simp [h]
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t : (↑I : Type)
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)
⊢ γ.subpath t t = refl ((γ : (a : (↑I : Type)) → X) t)

Tactic:
ext s
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t 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:
simp [subpath]

Premises used: Path.subpath
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
a₁ :
  ∀ (s : (↑I : Type)),
    Eq (α := X) ((γ.subpath 0 1 : (a : (↑I : Type)) → X) s : X) ((γ.cast ⋯ ⋯ : (a : (↑I : Type)) → X) s : X)
⊢ γ.subpath 0 1 = γ.cast ⋯ ⋯

Tactic:
ext s
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
s : (↑I : Type)
⊢ Eq (α := X) ((γ.subpath 0 1 : (a : (↑I : Type)) → X) s : X) ((γ.cast ⋯ ⋯ : (a : (↑I : Type)) → X) s : X)

Tactic:
simp [subpath]

Premises used: Path.subpath
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
⊢ Continuous.{0, u_1} (Y := X) fun (x : (↑I : Type) × (↑I : Type) × (↑I : Type)) ↦
    (γ.subpath x.1 x.2.1 : (a : (↑I : Type)) → X) x.2.2

Tactic:
Continuous.comp' (map_continuous γ) Set.Icc.continuous_convexComb_prod

Premises used: Continuous.comp', ContinuousMapClass.map_continuous, Set.Icc.continuous_convexComb_prod
-- Module: Mathlib.Topology.Subpath
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

Tactic:
Path.trans_continuous_family γ₁ ?_ γ₂ ?_

Premises used: Path.trans_continuous_family
-- Module: Mathlib.Topology.Subpath
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 ↿γ₁
refine_2 : 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

Tactic:
refine Path.trans_continuous_family γ₁ ?_ γ₂ ?_

Premises used: Path.trans_continuous_family
-- Module: Mathlib.Topology.Subpath
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 ↿γ₁

Tactic:
γ.subpath_continuous_family.comp (.prodMk ?_ <| .prodMk ?_ ?_)

Premises used: Set.Icc.convexComb, Continuous.comp, Path.subpath_continuous_family, Continuous.prodMk
-- Module: Mathlib.Topology.Subpath
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₂ : ℝ)) ⋯
refine_1₂ : Continuous (Y := (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦ x.2
⊢ Continuous ↿γ₁

Tactic:
refine γ.subpath_continuous_family.comp (.prodMk ?_ <| .prodMk ?_ ?_)

Premises used: Continuous.comp, Path.subpath_continuous_family, Continuous.prodMk
-- Module: Mathlib.Topology.Subpath
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 ↿γ₂

Tactic:
γ.subpath_continuous_family.comp (.prodMk ?_ <| .prodMk ?_ ?_)

Premises used: Set.Icc.convexComb, Continuous.comp, Path.subpath_continuous_family, Continuous.prodMk
-- Module: Mathlib.Topology.Subpath
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₂
refine_2₂ : Continuous (Y := (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦ x.2
⊢ Continuous ↿γ₂

Tactic:
refine γ.subpath_continuous_family.comp (.prodMk ?_ <| .prodMk ?_ ?_)

Premises used: Continuous.comp, Path.subpath_continuous_family, Continuous.prodMk
-- Module: Mathlib.Topology.Subpath
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 (Y := (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦ t₀

Tactic:
fun_prop
-- Module: Mathlib.Topology.Subpath
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 (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₂ : ℝ)) ⋯

Tactic:
fun_prop
-- Module: Mathlib.Topology.Subpath
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 (Y := (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦ x.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.Subpath
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 (Y := (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦ t₂

Tactic:
fun_prop
-- Module: Mathlib.Topology.Subpath
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [Icc.convexComb_zero, coe_toContinuousMap]

Premises used: Set.Icc.convexComb_zero, Path.coe_toContinuousMap