awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F_1 : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
G : f₁.HomotopyRel f₂ S
t : (↑I : Type)
x : X
hx : x ∈ S
simp :
  Eq.{v + 1} (α := Y)
    (({
            toFun := fun (x : X) ↦
              if (↑t : ℝ) ≤ 1 / 2 then
                (((F.toHomotopy (P := fun (f : C(X, Y)) ↦
                              ∀ x ∈ S,
                                Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₀ : (a : X) → Y) x : Y)).extend :
                          (a : ℝ) → C(X, Y))
                        (2 * (↑t : ℝ)) :
                      C(X, Y)) :
                    (a : X) → Y)
                  x
              else
                (((G.toHomotopy (P := fun (f : C(X, Y)) ↦
                              ∀ x ∈ S,
                                Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₁ : (a : X) → Y) x : Y)).extend :
                          (a : ℝ) → C(X, Y))
                        (2 * (↑t : ℝ) - 1) :
                      C(X, Y)) :
                    (a : X) → Y)
                  x,
            continuous_toFun := ⋯ : C(X, Y) } :
          (a : X) → Y)
        x :
      Y)
    ((f₀ : (a : X) → Y) x : Y)
⊢ Eq.{v + 1} (α := Y)
    (({
            toFun := fun (x : X) ↦
              (F.toHomotopy (P := fun (f : C(X, Y)) ↦
                        ∀ x ∈ S, Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₀ : (a : X) → Y) x : Y)).trans
                    (G.toHomotopy (P := fun (f : C(X, Y)) ↦
                      ∀ x ∈ S, Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₁ : (a : X) → Y) x : Y)))).toFun
                (t, x),
            continuous_toFun := ⋯ : C(X, Y) } :
          (a : X) → Y)
        x :
      Y)
    ((f₀ : (a : X) → Y) x : Y)

Tactic:
simp only [Homotopy.trans]

Premises used: ContinuousMap.Homotopy.trans
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F_1 : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
G : f₁.HomotopyRel f₂ S
t : (↑I : Type)
x : X
hx : x ∈ S
pos :
  ∀ (h : (↑t : ℝ) ≤ 1 / 2),
    Eq.{v + 1} (α := Y)
      (({
              toFun := fun (x : X) ↦
                (((F.toHomotopy (P := fun (f : C(X, Y)) ↦
                              ∀ x ∈ S,
                                Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₀ : (a : X) → Y) x : Y)).extend :
                          (a : ℝ) → C(X, Y))
                        (2 * (↑t : ℝ)) :
                      C(X, Y)) :
                    (a : X) → Y)
                  x,
              continuous_toFun := ⋯ : C(X, Y) } :
            (a : X) → Y)
          x :
        Y)
      ((f₀ : (a : X) → Y) x : Y)
neg :
  ∀ (h : ¬(↑t : ℝ) ≤ 1 / 2),
    Eq.{v + 1} (α := Y)
      (({
              toFun := fun (x : X) ↦
                (((G.toHomotopy (P := fun (f : C(X, Y)) ↦
                              ∀ x ∈ S,
                                Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₁ : (a : X) → Y) x : Y)).extend :
                          (a : ℝ) → C(X, Y))
                        (2 * (↑t : ℝ) - 1) :
                      C(X, Y)) :
                    (a : X) → Y)
                  x,
              continuous_toFun := ⋯ : C(X, Y) } :
            (a : X) → Y)
          x :
        Y)
      ((f₀ : (a : X) → Y) x : Y)
⊢ Eq.{v + 1} (α := Y)
    (({
            toFun := fun (x : X) ↦
              if (↑t : ℝ) ≤ 1 / 2 then
                (((F.toHomotopy (P := fun (f : C(X, Y)) ↦
                              ∀ x ∈ S,
                                Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₀ : (a : X) → Y) x : Y)).extend :
                          (a : ℝ) → C(X, Y))
                        (2 * (↑t : ℝ)) :
                      C(X, Y)) :
                    (a : X) → Y)
                  x
              else
                (((G.toHomotopy (P := fun (f : C(X, Y)) ↦
                              ∀ x ∈ S,
                                Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₁ : (a : X) → Y) x : Y)).extend :
                          (a : ℝ) → C(X, Y))
                        (2 * (↑t : ℝ) - 1) :
                      C(X, Y)) :
                    (a : X) → Y)
                  x,
            continuous_toFun := ⋯ : C(X, Y) } :
          (a : X) → Y)
        x :
      Y)
    ((f₀ : (a : X) → Y) x : Y)

Tactic:
split_ifs
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F_1 : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
G : f₁.HomotopyRel f₂ S
t : (↑I : Type)
x : X
hx : x ∈ S
h : (↑t : ℝ) ≤ 1 / 2
⊢ Eq.{v + 1} (α := Y)
    (({
            toFun := fun (x : X) ↦
              (((F.toHomotopy (P := fun (f : C(X, Y)) ↦
                            ∀ x ∈ S, Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₀ : (a : X) → Y) x : Y)).extend :
                        (a : ℝ) → C(X, Y))
                      (2 * (↑t : ℝ)) :
                    C(X, Y)) :
                  (a : X) → Y)
                x,
            continuous_toFun := ⋯ : C(X, Y) } :
          (a : X) → Y)
        x :
      Y)
    ((f₀ : (a : X) → Y) x : Y)

Tactic:
simp [HomotopyWith.extendProp F (2 * t) x hx, F.fst_eq_snd hx, G.fst_eq_snd hx]

Premises used: ContinuousMap.HomotopyRel.fst_eq_snd, HMul.hMul, ContinuousMap.HomotopyWith.extendProp, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F_1 : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
G : f₁.HomotopyRel f₂ S
t : (↑I : Type)
x : X
hx : x ∈ S
h : ¬(↑t : ℝ) ≤ 1 / 2
⊢ Eq.{v + 1} (α := Y)
    (({
            toFun := fun (x : X) ↦
              (((G.toHomotopy (P := fun (f : C(X, Y)) ↦
                            ∀ x ∈ S, Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₁ : (a : X) → Y) x : Y)).extend :
                        (a : ℝ) → C(X, Y))
                      (2 * (↑t : ℝ) - 1) :
                    C(X, Y)) :
                  (a : X) → Y)
                x,
            continuous_toFun := ⋯ : C(X, Y) } :
          (a : X) → Y)
        x :
      Y)
    ((f₀ : (a : X) → Y) x : Y)

Tactic:
simp [HomotopyWith.extendProp G (2 * t - 1) x hx, F.fst_eq_snd hx, G.fst_eq_snd hx]

Premises used: ContinuousMap.HomotopyRel.fst_eq_snd, HMul.hMul, HSub.hSub, ContinuousMap.HomotopyWith.extendProp, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
G : f₁.HomotopyRel f₂ S
x : (↑I : Type) × X
⊢ Eq.{v + 1} (α := Y) ((F.trans (S := S) G : (a : (↑I : Type) × X) → Y) x : Y)
    (if h : (↑x.1 : ℝ) ≤ 1 / 2 then
        (F : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ)) ⋯, x.2)
      else (G : (a : (↑I : Type) × X) → Y) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.1 : ℝ) - 1) ⋯, x.2) :
      Y)

Tactic:
Homotopy.trans_apply _ _ _

Premises used: ContinuousMap.Homotopy.trans_apply
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
G : f₁.HomotopyRel f₂ S
⊢ (F.trans (S := S) G).symm (S := S) = G.symm (S := S).trans (S := S) (F.symm (S := S))

Tactic:
HomotopyWith.ext <| Homotopy.congr_fun <| Homotopy.symm_trans _ _

Premises used: ContinuousMap.Homotopy.symm_trans, ContinuousMap.HomotopyWith.ext, ContinuousMap.Homotopy.congr_fun
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
F_1 : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
f₀_1 f₁_1 f₂ : C(X, Y)
S : Set X
f₀ f₁ g₀ g₁ : C(X, Y)
F : f₀.HomotopyRel f₁ S
h₀ : f₀ = g₀
h₁ : f₁ = g₁
t : (↑I : Type)
x : X
hx : x ∈ S
⊢ Eq.{v + 1} (α := Y)
    (({
            toFun := fun (x : X) ↦
              (F.toHomotopy (P := fun (f : C(X, Y)) ↦
                        ∀ x ∈ S, Eq.{v + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f₀ : (a : X) → Y) x : Y)).cast
                    h₀ h₁).toFun
                (t, x),
            continuous_toFun := ⋯ : C(X, Y) } :
          (a : X) → Y)
        x :
      Y)
    ((g₀ : (a : X) → Y) x : Y)

Tactic:
simpa only [← h₀, ← h₁] using F.prop t x hx

Premises used: ContinuousMap.HomotopyWith.prop
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
S : Set X
f₀ f₁ : C(X, Y)
h : f₀.HomotopicRel f₁ S
⊢ f₀.Homotopic f₁

Tactic:
h.map fun F ↦ F.1

Premises used: ContinuousMap.Homotopic, Nonempty.map
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
S : Set X
f₀ f₁ : C(X, Y)
h : f₀.HomotopicRel f₁ S
x : X
hx : x ∈ S
⊢ Eq.{v + 1} (α := Y) ((f₀ : (a : X) → Y) x : Y) ((f₁ : (a : X) → Y) x : Y)

Tactic:
Nonempty.elim h (HomotopyRel.fst_eq_snd · hx)

Premises used: ContinuousMap.HomotopyRel.fst_eq_snd, Nonempty.elim
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
S : Set X
f : C(X, Y)
⊢ f.HomotopicRel f S

Tactic:
⟨HomotopyRel.refl f S⟩

Premises used: ContinuousMap.HomotopicRel, Nonempty.intro, ContinuousMap.HomotopyRel.refl
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
S : Set X
f g : C(X, Y)
h : f.HomotopicRel g S
⊢ g.HomotopicRel f S

Tactic:
h.map HomotopyRel.symm

Premises used: ContinuousMap.HomotopyRel.symm, ContinuousMap.HomotopicRel, Nonempty.map
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
S : Set X
f g h : C(X, Y)
h₀ : f.HomotopicRel g S
h₁ : g.HomotopicRel h S
⊢ f.HomotopicRel h S

Tactic:
h₀.map2 HomotopyRel.trans h₁

Premises used: Nonempty.map2, ContinuousMap.HomotopicRel, ContinuousMap.HomotopyRel.trans
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
S : Set X
⊢ ∀ {x y : C(X, Y)}, x.HomotopicRel y S → y.HomotopicRel x S

Tactic:
apply symm

Premises used: ContinuousMap.HomotopicRel.symm
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
S : Set X
⊢ ∀ {x y z : C(X, Y)}, x.HomotopicRel y S → y.HomotopicRel z S → x.HomotopicRel z S

Tactic:
apply trans

Premises used: ContinuousMap.HomotopicRel.trans
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
Z : Type w
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
S : Set X
f₀ f₁ : C(X, Y)
h : f₀.HomotopicRel f₁ S
g : C(Y, Z)
⊢ (g.comp f₀).HomotopicRel (g.comp f₁) S

Tactic:
h.map (·.compContinuousMap g)

Premises used: ContinuousMap.HomotopicRel, Nonempty.map
-- Module: Mathlib.Topology.Homotopy.Basic
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f₀ f₁ : C(X, Y)
⊢ f₀.HomotopicRel f₁ ∅ ↔ f₀.Homotopic f₁

Tactic:
⟨fun h ↦ h.homotopic, fun ⟨F⟩ ↦ ⟨⟨F, fun _ _ ↦ False.elim⟩⟩⟩

Premises used: False.elim, ContinuousMap.HomotopicRel, ContinuousMap.HomotopyWith.mk, _private.0.ContinuousMap.homotopicRel_empty.match_1, Nonempty.intro, Iff.intro, ContinuousMap.HomotopicRel.homotopic, EmptyCollection.emptyCollection
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
y : Y
⊢ Homotopic (const X y) (const X y)

Tactic:
rfl
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
hf : f.Nullhomotopic
g : C(Y, Z)
obtain : ∀ (y : Y) (hy : f.Homotopic (const X y)), (g.comp f).Nullhomotopic
⊢ (g.comp f).Nullhomotopic

Tactic:
obtain ⟨y, hy⟩ := hf
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
g : C(Y, Z)
y : Y
hy : f.Homotopic (const X y)
h : (g.comp f).Homotopic (const X ((g : (a : Y) → Z) y))
⊢ (g.comp f).Nullhomotopic

Tactic:
use g y

Premises used: DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
g : C(Y, Z)
y : Y
hy : f.Homotopic (const X y)
⊢ (g.comp f).Homotopic (const X ((g : (a : Y) → Z) y))

Tactic:
.comp (.refl g) hy

Premises used: ContinuousMap.Homotopic.comp, ContinuousMap.comp, ContinuousMap.const, ContinuousMap.Homotopic.refl
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
g : C(Y, Z)
y : Y
hy : f.Homotopic (const X y)
⊢ (g.comp f).Homotopic (const X ((g : (a : Y) → Z) y))

Tactic:
exact .comp (.refl g) hy
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(Y, Z)
hf : f.Nullhomotopic
g : C(X, Y)
obtain : ∀ (y : Z) (hy : f.Homotopic (const Y y)), (f.comp g).Nullhomotopic
⊢ (f.comp g).Nullhomotopic

Tactic:
obtain ⟨y, hy⟩ := hf
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(Y, Z)
g : C(X, Y)
y : Z
hy : f.Homotopic (const Y y)
h : (f.comp g).Homotopic (const X y)
⊢ (f.comp g).Nullhomotopic

Tactic:
use y
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(Y, Z)
g : C(X, Y)
y : Z
hy : f.Homotopic (const Y y)
⊢ (f.comp g).Homotopic (const X y)

Tactic:
.comp hy (.refl g)

Premises used: ContinuousMap.Homotopic.comp, ContinuousMap.comp, ContinuousMap.const, ContinuousMap.Homotopic.refl
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(Y, Z)
g : C(X, Y)
y : Z
hy : f.Homotopic (const Y y)
⊢ (f.comp g).Homotopic (const X y)

Tactic:
exact .comp hy (.refl g)
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : ContractibleSpace X
⊢ Nonempty.{max 1 (u_1 + 1)} (X ≃ₕ Unit)

Tactic:
ContractibleSpace.hequiv_unit'

Premises used: ContractibleSpace.hequiv_unit'
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : ContractibleSpace X
obtain : ∀ (hv : X ≃ₕ Unit), Nullhomotopic (ContinuousMap.id X)
⊢ Nullhomotopic (ContinuousMap.id X)

Tactic:
obtain ⟨hv⟩ := ContractibleSpace.hequiv_unit X

Premises used: ContractibleSpace.hequiv_unit
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : ContractibleSpace X
hv : X ≃ₕ Unit
h : Homotopic (ContinuousMap.id X) (const X ((hv.invFun : (a : Unit) → X) ()))
⊢ Nullhomotopic (ContinuousMap.id X)

Tactic:
use hv.invFun ()

Premises used: Unit.unit, ContinuousMap.HomotopyEquiv.invFun, DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : ContractibleSpace X
hv : X ≃ₕ Unit
⊢ Homotopic (ContinuousMap.id X) (hv.invFun.comp hv.toFun)

Tactic:
hv.left_inv.symm

Premises used: ContinuousMap.Homotopic.symm, ContinuousMap.HomotopyEquiv.left_inv
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : ContractibleSpace X
hv : X ≃ₕ Unit
⊢ Homotopic (ContinuousMap.id X) (const X ((hv.invFun : (a : Unit) → X) ()))

Tactic:
convert! hv.left_inv.symm

Premises used: ContinuousMap.Homotopic.symm, ContinuousMap.HomotopyEquiv.left_inv
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
Y : Type u_1
inst : TopologicalSpace Y
mp : ContractibleSpace Y → Nullhomotopic (ContinuousMap.id Y)
mpr : Nullhomotopic (ContinuousMap.id Y) → ContractibleSpace Y
⊢ ContractibleSpace Y ↔ Nullhomotopic (ContinuousMap.id Y)

Tactic:
constructor
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
Y : Type u_1
inst : TopologicalSpace Y
h : ContractibleSpace Y
⊢ Nullhomotopic (ContinuousMap.id Y)

Tactic:
apply id_nullhomotopic

Premises used: id_nullhomotopic
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
Y : Type u_1
inst : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
⊢ ContractibleSpace Y

Tactic:
{ hequiv_unit' :=
        ⟨{  toFun := ContinuousMap.const _ ()
            invFun := ContinuousMap.const _ p
            left_inv := ?_
            right_inv := ?_ }⟩ }

Premises used: Unit.unit, ContinuousMap.HomotopyEquiv.mk, ContractibleSpace.mk, Nonempty.intro, Unit, ContinuousMap.const
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
Y : Type u_1
inst : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
mpr : Homotopic (comp (const Unit p) (const Y ())) (ContinuousMap.id Y)
mpr₁ : Homotopic (comp (const Y ()) (const Unit p)) (ContinuousMap.id Unit)
⊢ ContractibleSpace Y

Tactic:
refine
    { hequiv_unit' :=
        ⟨{  toFun := ContinuousMap.const _ ()
            invFun := ContinuousMap.const _ p
            left_inv := ?_
            right_inv := ?_ }⟩ }
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
Y : Type u_1
inst : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
⊢ Homotopic (comp (const Unit p) (const Y ())) (ContinuousMap.id Y)

Tactic:
h.symm

Premises used: ContinuousMap.comp, ContinuousMap.Homotopic.symm, ContinuousMap.const
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
Y : Type u_1
inst : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
⊢ Homotopic (comp (const Unit p) (const Y ())) (ContinuousMap.id Y)

Tactic:
exact h.symm

Premises used: ContinuousMap.Homotopic.symm
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
Y : Type u_1
inst : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
⊢ Homotopic (ContinuousMap.id Unit) (ContinuousMap.id Unit)

Tactic:
Homotopic.refl (ContinuousMap.id Unit)

Premises used: ContinuousMap.id, Unit, ContinuousMap.Homotopic.refl
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
Y : Type u_1
inst : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
⊢ Homotopic (comp (const Y ()) (const Unit p)) (ContinuousMap.id Unit)

Tactic:
convert! Homotopic.refl (ContinuousMap.id Unit)

Premises used: ContinuousMap.id, Unit, ContinuousMap.Homotopic.refl
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace Y
e : X ≃ₕ Y
⊢ ContractibleSpace X

Tactic:
⟨(ContractibleSpace.hequiv_unit Y).map e.trans⟩

Premises used: ContractibleSpace.mk, ContinuousMap.HomotopyEquiv.trans, ContractibleSpace.hequiv_unit, Nonempty.map
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ₕ Y
⊢ ContractibleSpace X ↔ ContractibleSpace Y

Tactic:
⟨fun _ => e.symm.contractibleSpace, fun _ => e.contractibleSpace⟩

Premises used: ContinuousMap.HomotopyEquiv.contractibleSpace, ContinuousMap.HomotopyEquiv.symm, Iff.intro
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ContractibleSpace Y
e : X ≃ₜ Y
⊢ ContractibleSpace X

Tactic:
e.toHomotopyEquiv.contractibleSpace

Premises used: ContinuousMap.HomotopyEquiv.contractibleSpace, Homeomorph.toHomotopyEquiv
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ₜ Y
⊢ ContractibleSpace X ↔ ContractibleSpace Y

Tactic:
e.toHomotopyEquiv.contractibleSpace_iff

Premises used: Homeomorph.toHomotopyEquiv, ContinuousMap.HomotopyEquiv.contractibleSpace_iff
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : IndiscreteTopology Y
f g : C(X, Y)
⊢ ∀ (x : X),
    Eq.{u_2 + 1} (α := Y)
      (ContinuousMap.toFun (X := (↑unitInterval : Type) × X)
          {
            toFun := fun (x : (↑unitInterval : Type) × X) ↦
              match (motive := (↑unitInterval : Type) × X → Y) x with
              | (t, a) => if t = 0 then (f : (a : X) → Y) a else (g : (a : X) → Y) a,
            continuous_toFun := ⋯ }
          (0, x) :
        Y)
      ((f : (a : X) → Y) x : Y)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : IndiscreteTopology Y
f g : C(X, Y)
⊢ ∀ (x : X),
    Eq.{u_2 + 1} (α := Y)
      (ContinuousMap.toFun (X := (↑unitInterval : Type) × X)
          {
            toFun := fun (x : (↑unitInterval : Type) × X) ↦
              match (motive := (↑unitInterval : Type) × X → Y) x with
              | (t, a) => if t = 0 then (f : (a : X) → Y) a else (g : (a : X) → Y) a,
            continuous_toFun := ⋯ }
          (1, x) :
        Y)
      ((g : (a : X) → Y) x : Y)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Nonempty Y
inst_3 : IndiscreteTopology Y
f : C(X, Y)
inhabit : ∀ (inhabited_h : Inhabited Y), f.Nullhomotopic
⊢ f.Nullhomotopic

Tactic:
inhabit Y
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Nonempty Y
inst_3 : IndiscreteTopology Y
f : C(X, Y)
inhabited_h : Inhabited Y
h : f.Homotopic (const X default)
⊢ f.Nullhomotopic

Tactic:
use default

Premises used: Inhabited.default
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Nonempty Y
inst_3 : IndiscreteTopology Y
f : C(X, Y)
inhabited_h : Inhabited Y
⊢ f.Homotopic (const X default)

Tactic:
homotopic_of_indiscrete _ _

Premises used: homotopic_of_indiscrete
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Nonempty Y
inst_3 : IndiscreteTopology Y
f : C(X, Y)
inhabited_h : Inhabited Y
⊢ f.Homotopic (const X default)

Tactic:
exact homotopic_of_indiscrete _ _

Premises used: homotopic_of_indiscrete
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Nonempty Y
inst_3 : Subsingleton Y
⊢ ContractibleSpace Y

Tactic:
let ⟨_⟩ := nonempty_unique Y
  ⟨⟨(Homeomorph.homeomorphOfUnique Y Unit).toHomotopyEquiv⟩⟩

Premises used: ContractibleSpace.mk, Homeomorph.homeomorphOfUnique, ContractibleSpace, Homeomorph.toHomotopyEquiv, _private.0.ContractibleSpace.instOfNonemptyOfSubsingleton.match_1, Nonempty.intro, Unit, nonempty_unique
-- Module: Mathlib.Topology.Homotopy.Contractible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Nonempty Y
inst_3 : IndiscreteTopology Y
⊢ ContractibleSpace Y

Tactic:
(contractible_iff_id_nullhomotopic Y).mpr (nullhomotopic_of_indiscrete _)

Premises used: Iff.mpr, contractible_iff_id_nullhomotopic, nullhomotopic_of_indiscrete