awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
ι : Type u_3
inst_2 : StronglyLocallyContractibleSpace X
inst_3 : StronglyLocallyContractibleSpace Y
refine_1 :
  ∀ (x : X × Y),
    (𝓝 x).HasBasis (ι := Prod.{u_1, u_2} (Set X) (Set Y))
      ((fun (x : X × Y) (x_1 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
          (match (motive := X × Y → Prop) x with
            | (x, y) =>
              match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Prop) x_1 with
              | (Ux, Uy) =>
                (Ux ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑Ux : Type u_1)) ∧
                  Uy ∈ 𝓝 y ∧ ContractibleSpace.{u_2} (↑Uy : Type u_2) :
            Prop))
        x)
      ((fun (x : X × Y) (x_1 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
          (match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Set (X × Y)) x_1 with
            | (Ux, Uy) => Ux ×ˢ Uy :
            Set (X × Y)))
        x)
refine_2 :
  ∀ (x : X × Y) (i : Prod.{u_1, u_2} (Set X) (Set Y)),
    (fun (x : X × Y) (x_1 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
          (match (motive := X × Y → Prop) x with
            | (x, y) =>
              match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Prop) x_1 with
              | (Ux, Uy) =>
                (Ux ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑Ux : Type u_1)) ∧
                  Uy ∈ 𝓝 y ∧ ContractibleSpace.{u_2} (↑Uy : Type u_2) :
            Prop))
        x i →
      ContractibleSpace
        (↑((fun (x : X × Y) (x_1 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
                (match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Set (X × Y)) x_1 with
                  | (Ux, Uy) => Ux ×ˢ Uy :
                  Set (X × Y)))
              x i) :
          Type (max u_1 u_2))
⊢ StronglyLocallyContractibleSpace (X × Y)

Tactic:
refine .of_bases (ι := Set X × Set Y)
    (p := fun (x, y) (Ux, Uy) =>
      (Ux ∈ 𝓝 x ∧ ContractibleSpace Ux) ∧ (Uy ∈ 𝓝 y ∧ ContractibleSpace Uy))
    (s := fun _ (Ux, Uy) => Ux ×ˢ Uy) ?_ ?_
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 : X
ι : Type u_3
inst_2 : StronglyLocallyContractibleSpace X
inst_3 : StronglyLocallyContractibleSpace Y
x : X
y : Y
refine_1 :
  (𝓝 x ×ˢ 𝓝 y).HasBasis (ι := Prod.{u_1, u_2} (Set X) (Set Y))
    ((fun (x : X × Y) (x_2 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
        (match (motive := X × Y → Prop) x with
          | (x, y) =>
            match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Prop) x_2 with
            | (Ux, Uy) =>
              (Ux ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑Ux : Type u_1)) ∧
                Uy ∈ 𝓝 y ∧ ContractibleSpace.{u_2} (↑Uy : Type u_2) :
          Prop))
      (x, y))
    ((fun (x : X × Y) (x_2 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
        (match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Set (X × Y)) x_2 with
          | (Ux, Uy) => Ux ×ˢ Uy :
          Set (X × Y)))
      (x, y))
⊢ (𝓝 (x, y)).HasBasis (ι := Prod.{u_1, u_2} (Set X) (Set Y))
    ((fun (x : X × Y) (x_2 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
        (match (motive := X × Y → Prop) x with
          | (x, y) =>
            match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Prop) x_2 with
            | (Ux, Uy) =>
              (Ux ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑Ux : Type u_1)) ∧
                Uy ∈ 𝓝 y ∧ ContractibleSpace.{u_2} (↑Uy : Type u_2) :
          Prop))
      (x, y))
    ((fun (x : X × Y) (x_2 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
        (match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Set (X × Y)) x_2 with
          | (Ux, Uy) => Ux ×ˢ Uy :
          Set (X × Y)))
      (x, y))

Tactic:
rw [nhds_prod_eq]

Premises used: nhds_prod_eq
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 : X
ι : Type u_3
inst_2 : StronglyLocallyContractibleSpace X
inst_3 : StronglyLocallyContractibleSpace Y
x : X
y : Y
⊢ (𝓝 x ×ˢ 𝓝 y).HasBasis (ι := Prod.{u_1, u_2} (Set X) (Set Y))
    ((fun (x : X × Y) (x_2 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
        (match (motive := X × Y → Prop) x with
          | (x, y) =>
            match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Prop) x_2 with
            | (Ux, Uy) =>
              (Ux ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑Ux : Type u_1)) ∧
                Uy ∈ 𝓝 y ∧ ContractibleSpace.{u_2} (↑Uy : Type u_2) :
          Prop))
      (x, y))
    ((fun (x : X × Y) (x_2 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
        (match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Set (X × Y)) x_2 with
          | (Ux, Uy) => Ux ×ˢ Uy :
          Set (X × Y)))
      (x, y))

Tactic:
(contractible_basis x).prod (contractible_basis y)

Premises used: StronglyLocallyContractibleSpace.contractible_basis, Filter.HasBasis.prod
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 : X
ι : Type u_3
inst_2 : StronglyLocallyContractibleSpace X
inst_3 : StronglyLocallyContractibleSpace Y
x : X
y : Y
⊢ (𝓝 x ×ˢ 𝓝 y).HasBasis (ι := Prod.{u_1, u_2} (Set X) (Set Y))
    ((fun (x : X × Y) (x_2 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
        (match (motive := X × Y → Prop) x with
          | (x, y) =>
            match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Prop) x_2 with
            | (Ux, Uy) =>
              (Ux ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑Ux : Type u_1)) ∧
                Uy ∈ 𝓝 y ∧ ContractibleSpace.{u_2} (↑Uy : Type u_2) :
          Prop))
      (x, y))
    ((fun (x : X × Y) (x_2 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
        (match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Set (X × Y)) x_2 with
          | (Ux, Uy) => Ux ×ˢ Uy :
          Set (X × Y)))
      (x, y))

Tactic:
exact (contractible_basis x).prod (contractible_basis y)

Premises used: StronglyLocallyContractibleSpace.contractible_basis, Filter.HasBasis.prod
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 : X
ι : Type u_3
inst_2 : StronglyLocallyContractibleSpace X
inst_3 : StronglyLocallyContractibleSpace Y
x : X
y : Y
refine_2 :
  ∀ (Ux : Set X) (Uy : Set Y),
    (fun (x : X × Y) (x_2 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
          (match (motive := X × Y → Prop) x with
            | (x, y) =>
              match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Prop) x_2 with
              | (Ux, Uy) =>
                (Ux ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑Ux : Type u_1)) ∧
                  Uy ∈ 𝓝 y ∧ ContractibleSpace.{u_2} (↑Uy : Type u_2) :
            Prop))
        (x, y) (Ux, Uy) →
      ContractibleSpace
        (↑((fun (x : X × Y) (x_2 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
                (match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Set (X × Y)) x_2 with
                  | (Ux, Uy) => Ux ×ˢ Uy :
                  Set (X × Y)))
              (x, y) (Ux, Uy)) :
          Type (max u_1 u_2))
⊢ ∀ (i : Prod.{u_1, u_2} (Set X) (Set Y)),
    (fun (x : X × Y) (x_2 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
          (match (motive := X × Y → Prop) x with
            | (x, y) =>
              match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Prop) x_2 with
              | (Ux, Uy) =>
                (Ux ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑Ux : Type u_1)) ∧
                  Uy ∈ 𝓝 y ∧ ContractibleSpace.{u_2} (↑Uy : Type u_2) :
            Prop))
        (x, y) i →
      ContractibleSpace
        (↑((fun (x : X × Y) (x_2 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
                (match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Set (X × Y)) x_2 with
                  | (Ux, Uy) => Ux ×ˢ Uy :
                  Set (X × Y)))
              (x, y) i) :
          Type (max u_1 u_2))

Tactic:
(Ux, Uy)
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 : X
ι : Type u_3
inst_2 : StronglyLocallyContractibleSpace X
inst_3 : StronglyLocallyContractibleSpace Y
x : X
y : Y
Ux : Set X
Uy : Set Y
refine_2 :
  ∀ (hUx : Ux ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑Ux : Type u_1))
    (hUy : Uy ∈ 𝓝 y ∧ ContractibleSpace.{u_2} (↑Uy : Type u_2)),
    ContractibleSpace
      (↑((fun (x : X × Y) (x_2 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
              (match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Set (X × Y)) x_2 with
                | (Ux, Uy) => Ux ×ˢ Uy :
                Set (X × Y)))
            (x, y) (Ux, Uy)) :
        Type (max u_1 u_2))
⊢ (fun (x : X × Y) (x_2 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
        (match (motive := X × Y → Prop) x with
          | (x, y) =>
            match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Prop) x_2 with
            | (Ux, Uy) =>
              (Ux ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑Ux : Type u_1)) ∧
                Uy ∈ 𝓝 y ∧ ContractibleSpace.{u_2} (↑Uy : Type u_2) :
          Prop))
      (x, y) (Ux, Uy) →
    ContractibleSpace
      (↑((fun (x : X × Y) (x_2 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
              (match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Set (X × Y)) x_2 with
                | (Ux, Uy) => Ux ×ˢ Uy :
                Set (X × Y)))
            (x, y) (Ux, Uy)) :
        Type (max u_1 u_2))

Tactic:
⟨hUx, hUy⟩
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 : X
ι : Type u_3
inst_2 : StronglyLocallyContractibleSpace X
inst_3 : StronglyLocallyContractibleSpace Y
x : X
y : Y
Ux : Set X
Uy : Set Y
hUx : Ux ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑Ux : Type u_1)
hUy : Uy ∈ 𝓝 y ∧ ContractibleSpace.{u_2} (↑Uy : Type u_2)
⊢ ContractibleSpace.{u_1} (↑Ux : Type u_1)

Tactic:
haveI : ContractibleSpace Ux := hUx.2
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 : X
ι : Type u_3
inst_2 : StronglyLocallyContractibleSpace X
inst_3 : StronglyLocallyContractibleSpace Y
x : X
y : Y
Ux : Set X
Uy : Set Y
hUx : Ux ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑Ux : Type u_1)
hUy : Uy ∈ 𝓝 y ∧ ContractibleSpace.{u_2} (↑Uy : Type u_2)
this : ContractibleSpace.{u_1} (↑Ux : Type u_1)
⊢ ContractibleSpace.{u_2} (↑Uy : Type u_2)

Tactic:
haveI : ContractibleSpace Uy := hUy.2
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 : X
ι : Type u_3
inst_2 : StronglyLocallyContractibleSpace X
inst_3 : StronglyLocallyContractibleSpace Y
x : X
y : Y
Ux : Set X
Uy : Set Y
hUx : Ux ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑Ux : Type u_1)
hUy : Uy ∈ 𝓝 y ∧ ContractibleSpace.{u_2} (↑Uy : Type u_2)
this_1 : ContractibleSpace.{u_1} (↑Ux : Type u_1)
this : ContractibleSpace.{u_2} (↑Uy : Type u_2)
⊢ ContractibleSpace
    (↑((fun (x : X × Y) (x_2 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
            (match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Set (X × Y)) x_2 with
              | (Ux, Uy) => Ux ×ˢ Uy :
              Set (X × Y)))
          (x, y) (Ux, Uy)) :
      Type (max u_1 u_2))

Tactic:
(Homeomorph.Set.prod Ux Uy).contractibleSpace

Premises used: Homeomorph.contractibleSpace, Set.Mem, Homeomorph.Set.prod
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 : X
ι : Type u_3
inst_2 : StronglyLocallyContractibleSpace X
inst_3 : StronglyLocallyContractibleSpace Y
x : X
y : Y
Ux : Set X
Uy : Set Y
hUx : Ux ∈ 𝓝 x ∧ ContractibleSpace.{u_1} (↑Ux : Type u_1)
hUy : Uy ∈ 𝓝 y ∧ ContractibleSpace.{u_2} (↑Uy : Type u_2)
this_1 : ContractibleSpace.{u_1} (↑Ux : Type u_1)
this : ContractibleSpace.{u_2} (↑Uy : Type u_2)
⊢ ContractibleSpace
    (↑((fun (x : X × Y) (x_2 : Prod.{u_1, u_2} (Set X) (Set Y)) ↦
            (match (motive := Prod.{u_1, u_2} (Set X) (Set Y) → Set (X × Y)) x_2 with
              | (Ux, Uy) => Ux ×ˢ Uy :
              Set (X × Y)))
          (x, y) (Ux, Uy)) :
      Type (max u_1 u_2))

Tactic:
exact (Homeomorph.Set.prod Ux Uy).contractibleSpace

Premises used: Homeomorph.contractibleSpace, Homeomorph.Set.prod
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : StronglyLocallyContractibleSpace X
x : X
U : Set X
hU : U ∈ 𝓝 x
obtain :
  ∀ (V : Set X) (hVU : id V ⊆ U) (hVmem : V ∈ 𝓝 x) (hVcontractible : ContractibleSpace.{u_1} (↑V : Type u_1)),
    ∃ (V : Set X) (hVU : V ⊆ U), V ∈ 𝓝 x ∧ Nullhomotopic (ContinuousMap.inclusion (s := V) (t := U) hVU)
⊢ ∃ (V : Set X) (hVU : V ⊆ U), V ∈ 𝓝 x ∧ Nullhomotopic (ContinuousMap.inclusion (s := V) (t := U) hVU)

Tactic:
obtain ⟨V, ⟨hVmem, hVcontractible⟩, hVU⟩ := (contractible_basis x).mem_iff.mp hU

Premises used: Filter.HasBasis.mem_iff, StronglyLocallyContractibleSpace.contractible_basis, Iff.mp
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : StronglyLocallyContractibleSpace X
x : X
U : Set X
hU : U ∈ 𝓝 x
V : Set X
hVU : id V ⊆ U
hVmem : V ∈ 𝓝 x
hVcontractible : ContractibleSpace.{u_1} (↑V : Type u_1)
⊢ ∃ (V : Set X) (hVU : V ⊆ U), V ∈ 𝓝 x ∧ Nullhomotopic (ContinuousMap.inclusion (s := V) (t := U) hVU)

Tactic:
⟨V, hVU, hVmem, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : StronglyLocallyContractibleSpace X
x : X
U : Set X
hU : U ∈ 𝓝 x
V : Set X
hVU : id V ⊆ U
hVmem : V ∈ 𝓝 x
hVcontractible : ContractibleSpace.{u_1} (↑V : Type u_1)
refine : Nullhomotopic (ContinuousMap.inclusion (s := V) (t := U) hVU)
⊢ ∃ (V : Set X) (hVU : V ⊆ U), V ∈ 𝓝 x ∧ Nullhomotopic (ContinuousMap.inclusion (s := V) (t := U) hVU)

Tactic:
refine ⟨V, hVU, hVmem, ?_⟩
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : StronglyLocallyContractibleSpace X
x : X
U : Set X
hU : U ∈ 𝓝 x
V : Set X
hVU : id V ⊆ U
hVmem : V ∈ 𝓝 x
hVcontractible : ContractibleSpace.{u_1} (↑V : Type u_1)
obtain :
  ∀ (v₀ : (↑V : Type u_1))
    (hid : Homotopic (ContinuousMap.id (↑V : Type u_1)) (ContinuousMap.const (↑V : Type u_1) v₀)),
    Nullhomotopic (ContinuousMap.inclusion (s := V) (t := U) hVU)
⊢ Nullhomotopic (ContinuousMap.inclusion (s := V) (t := U) hVU)

Tactic:
obtain ⟨v₀, hid⟩ := id_nullhomotopic V

Premises used: Set.Elem, id_nullhomotopic
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : StronglyLocallyContractibleSpace X
x : X
U : Set X
hU : U ∈ 𝓝 x
V : Set X
hVU : id V ⊆ U
hVmem : V ∈ 𝓝 x
hVcontractible : ContractibleSpace.{u_1} (↑V : Type u_1)
v₀ : (↑V : Type u_1)
hid : Homotopic (ContinuousMap.id (↑V : Type u_1)) (ContinuousMap.const (↑V : Type u_1) v₀)
⊢ Nullhomotopic (ContinuousMap.inclusion (s := V) (t := U) hVU)

Tactic:
⟨ContinuousMap.inclusion hVU v₀, ?_⟩

Premises used: ContinuousMap.Nullhomotopic, ContinuousMap.inclusion, Exists.intro, DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : StronglyLocallyContractibleSpace X
x : X
U : Set X
hU : U ∈ 𝓝 x
V : Set X
hVU : id V ⊆ U
hVmem : V ∈ 𝓝 x
hVcontractible : ContractibleSpace.{u_1} (↑V : Type u_1)
v₀ : (↑V : Type u_1)
hid : Homotopic (ContinuousMap.id (↑V : Type u_1)) (ContinuousMap.const (↑V : Type u_1) v₀)
refine :
  Homotopic (ContinuousMap.inclusion (s := V) (t := U) hVU)
    (ContinuousMap.const (↑V : Type u_1)
      ((ContinuousMap.inclusion (s := id V) (t := U) hVU : (a : (↑(id V) : Type u_1)) → (↑U : Type u_1)) v₀))
⊢ Nullhomotopic (ContinuousMap.inclusion (s := V) (t := U) hVU)

Tactic:
refine ⟨ContinuousMap.inclusion hVU v₀, ?_⟩
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : StronglyLocallyContractibleSpace X
x : X
U : Set X
hU : U ∈ 𝓝 x
V : Set X
hVU : id V ⊆ U
hVmem : V ∈ 𝓝 x
hVcontractible : ContractibleSpace.{u_1} (↑V : Type u_1)
v₀ : (↑V : Type u_1)
hid : Homotopic (ContinuousMap.id (↑V : Type u_1)) (ContinuousMap.const (↑V : Type u_1) v₀)
⊢ Homotopic (ContinuousMap.comp (ContinuousMap.inclusion (s := id V) (t := U) hVU) (ContinuousMap.id (↑V : Type u_1)))
    (ContinuousMap.comp (ContinuousMap.inclusion (s := id V) (t := U) hVU) (ContinuousMap.const (↑V : Type u_1) v₀))

Tactic:
Homotopic.comp (.refl _) hid

Premises used: ContinuousMap.Homotopic.comp, ContinuousMap.Homotopic.refl
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : StronglyLocallyContractibleSpace X
x : X
U : Set X
hU : U ∈ 𝓝 x
V : Set X
hVU : id V ⊆ U
hVmem : V ∈ 𝓝 x
hVcontractible : ContractibleSpace.{u_1} (↑V : Type u_1)
v₀ : (↑V : Type u_1)
hid : Homotopic (ContinuousMap.id (↑V : Type u_1)) (ContinuousMap.const (↑V : Type u_1) v₀)
h :
  Eq (α := C((↑V : Type u_1), (↑U : Type u_1))) (ContinuousMap.inclusion (s := V) (t := U) hVU)
    (ContinuousMap.comp (ContinuousMap.inclusion (s := id V) (t := U) hVU) (ContinuousMap.id (↑V : Type u_1)))
⊢ Homotopic (ContinuousMap.inclusion (s := V) (t := U) hVU)
    (ContinuousMap.const (↑V : Type u_1)
      ((ContinuousMap.inclusion (s := id V) (t := U) hVU : (a : (↑(id V) : Type u_1)) → (↑U : Type u_1)) v₀))

Tactic:
convert! Homotopic.comp (.refl _) hid

Premises used: ContinuousMap.Homotopic.comp, ContinuousMap.Homotopic.refl
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : StronglyLocallyContractibleSpace X
x : X
U : Set X
hU : U ∈ 𝓝 x
V : Set X
hVU : id V ⊆ U
hVmem : V ∈ 𝓝 x
hVcontractible : ContractibleSpace.{u_1} (↑V : Type u_1)
v₀ : (↑V : Type u_1)
hid : Homotopic (ContinuousMap.id (↑V : Type u_1)) (ContinuousMap.const (↑V : Type u_1) v₀)
h :
  ∀ (a : (↑V : Type u_1)),
    Eq.{u_1 + 1} (α := X)
      (↑((ContinuousMap.inclusion (s := V) (t := U) hVU : (a : (↑V : Type u_1)) → (↑U : Type u_1)) a) : X)
      (↑((ContinuousMap.comp (ContinuousMap.inclusion (s := id V) (t := U) hVU) (ContinuousMap.id (↑V : Type u_1)) :
              (a : (↑V : Type u_1)) → (↑U : Type u_1))
            a) :
        X)
⊢ Eq (α := C((↑V : Type u_1), (↑U : Type u_1))) (ContinuousMap.inclusion (s := V) (t := U) hVU)
    (ContinuousMap.comp (ContinuousMap.inclusion (s := id V) (t := U) hVU) (ContinuousMap.id (↑V : Type u_1)))

Tactic:
ext
-- Module: Mathlib.Topology.Homotopy.LocallyContractible
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : StronglyLocallyContractibleSpace X
x : X
U : Set X
hU : U ∈ 𝓝 x
V : Set X
hVU : id V ⊆ U
hVmem : V ∈ 𝓝 x
hVcontractible : ContractibleSpace.{u_1} (↑V : Type u_1)
v₀ : (↑V : Type u_1)
hid : Homotopic (ContinuousMap.id (↑V : Type u_1)) (ContinuousMap.const (↑V : Type u_1) v₀)
a : (↑V : Type u_1)
⊢ Eq.{u_1 + 1} (α := X)
    (↑((ContinuousMap.inclusion (s := V) (t := U) hVU : (a : (↑V : Type u_1)) → (↑U : Type u_1)) a) : X)
    (↑((ContinuousMap.comp (ContinuousMap.inclusion (s := id V) (t := U) hVU) (ContinuousMap.id (↑V : Type u_1)) :
            (a : (↑V : Type u_1)) → (↑U : Type u_1))
          a) :
      X)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
⊢ Function.Injective.{u + 1, u + 1} (α := p₀.Homotopy p₁) (β := (↑I : Type) × (↑I : Type) → X)
    (DFunLike.coe (β := fun (x : (↑I : Type) × (↑I : Type)) ↦ X))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : (↑I : Type)
⊢ (F : (a : (↑I : Type) × (↑I : Type)) → X) (t, 0) = x₀

Tactic:
calc F (t, 0) = p₀ 0 := ContinuousMap.HomotopyRel.eq_fst _ _ (.inl rfl)
  _ = x₀ := p₀.source

Premises used: Trans.trans, Path.source, Or.inl, ContinuousMap.HomotopyRel.eq_fst, rfl
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : (↑I : Type)
⊢ (F : (a : (↑I : Type) × (↑I : Type)) → X) (t, 1) = x₁

Tactic:
calc F (t, 1) = p₀ 1 := ContinuousMap.HomotopyRel.eq_fst _ _ (.inr rfl)
  _ = x₁ := p₀.target

Premises used: Trans.trans, ContinuousMap.HomotopyRel.eq_fst, Path.target, Or.inr, rfl
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : (↑I : Type)
⊢ (((F.toHomotopy (P := fun (f : C((↑I : Type), X)) ↦
                  ∀ (x : (↑I : Type)),
                    Membership.mem (γ := Set (↑I : Type)) {0, 1} x →
                      Eq (α := X) ((f : (a : (↑I : Type)) → X) x : X)
                        ((p₀.toContinuousMap : (a : (↑I : Type)) → X) x : X)).curry :
              (a : (↑I : Type)) → C((↑I : Type), X))
            t :
          C((↑I : Type), X)) :
        (a : (↑I : Type)) → X)
      0 =
    x₀

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : (↑I : Type)
⊢ (((F.toHomotopy (P := fun (f : C((↑I : Type), X)) ↦
                  ∀ (x : (↑I : Type)),
                    Membership.mem (γ := Set (↑I : Type)) {0, 1} x →
                      Eq (α := X) ((f : (a : (↑I : Type)) → X) x : X)
                        ((p₀.toContinuousMap : (a : (↑I : Type)) → X) x : X)).curry :
              (a : (↑I : Type)) → C((↑I : Type), X))
            t :
          C((↑I : Type), X)) :
        (a : (↑I : Type)) → X)
      1 =
    x₁

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
a : ∀ (t : (↑I : Type)), Eq (α := X) ((F.eval 0 : (a : (↑I : Type)) → X) t : X) ((p₀ : (a : (↑I : Type)) → X) t : X)
⊢ F.eval 0 = p₀

Tactic:
ext t
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : (↑I : Type)
⊢ Eq (α := X) ((F.eval 0 : (a : (↑I : Type)) → X) t : X) ((p₀ : (a : (↑I : Type)) → X) t : X)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
a : ∀ (t : (↑I : Type)), Eq (α := X) ((F.eval 1 : (a : (↑I : Type)) → X) t : X) ((p₁ : (a : (↑I : Type)) → X) t : X)
⊢ F.eval 1 = p₁

Tactic:
ext t
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : (↑I : Type)
⊢ Eq (α := X) ((F.eval 1 : (a : (↑I : Type)) → X) t : X) ((p₁ : (a : (↑I : Type)) → X) t : X)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
⊢ F.symm.symm = F

Tactic:
ContinuousMap.HomotopyRel.symm_symm F

Premises used: Path.Homotopy.symm, ContinuousMap.HomotopyRel.symm_symm
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
⊢ Function.Bijective.{u + 1, u + 1} (α := p₀.Homotopy p₁) symm

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

Premises used: Iff.mpr, Function.bijective_iff_has_inverse, And.intro, Exists.intro, Path.Homotopy.symm_symm
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ p₂ : Path x₀ x₁
F : p₀.Homotopy p₁
G : p₁.Homotopy p₂
x : (↑I : Type) × (↑I : Type)
⊢ Eq (α := X) ((F.trans G : (a : (↑I : Type) × (↑I : Type)) → X) x : X)
    (if h : (↑x.1 : ℝ) ≤ 1 / 2 then
        (F : (a : (↑I : Type) × (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ)) ⋯, x.2)
      else
        (G : (a : (↑I : Type) × (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ) - 1) ⋯, x.2) :
      X)

Tactic:
ContinuousMap.HomotopyRel.trans_apply _ _ _

Premises used: ContinuousMap.HomotopyRel.trans_apply
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ p₂ : Path x₀ x₁
F : p₀.Homotopy p₁
G : p₁.Homotopy p₂
⊢ (F.trans G).symm = G.symm.trans F.symm

Tactic:
ContinuousMap.HomotopyRel.symm_trans _ _

Premises used: Path.Homotopy.trans, ContinuousMap.HomotopyRel.symm_trans, Path.Homotopy.symm