mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
y : Y
⊢ (const X y).Homotopic (const X y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : f.Nullhomotopic
g : C(Y, Z)
⊢ (g.comp f).Nullhomotopic

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(Y, Z)
hf : f.Nullhomotopic
g : C(X, Y)
⊢ (f.comp g).Nullhomotopic

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : ContractibleSpace X
⊢ (ContinuousMap.id X).Nullhomotopic

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ ContractibleSpace Y ↔ (ContinuousMap.id Y).Nullhomotopic

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : IndiscreteTopology Y
f g : C(X, Y)
⊢ ∀ (x : X),
    {
            toFun := fun x ↦
              match x with
              | (t, a) => if t = 0 then f a else g a,
            continuous_toFun := ⋯ }.toFun
        (0, x) =
      f x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : IndiscreteTopology Y
f g : C(X, Y)
⊢ ∀ (x : X),
    {
            toFun := fun x ↦
              match x with
              | (t, a) => if t = 0 then f a else g a,
            continuous_toFun := ⋯ }.toFun
        (1, x) =
      g x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Nonempty Y
inst✝ : IndiscreteTopology Y
f : C(X, Y)
⊢ f.Nullhomotopic

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : ContractibleSpace X
inst✝ : ContractibleSpace Y
⊢ Nonempty (X ≃ₕ Y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
⊢ PathConnectedSpace X

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : ContractibleSpace X
inst✝ : ContractibleSpace Y
⊢ ContractibleSpace (X × Y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x t : ↑I
ht : t ∈ {0, 1}
⊢ {
        toFun := fun x_1 ↦
          if ↑(x, x_1).2 ≤ 1 / 2 then (F.eval (x, x_1).1).extend (2 * ↑(x, x_1).2)
          else (G.eval (x, x_1).1).extend (2 * ↑(x, x_1).2 - 1),
        continuous_toFun := ⋯ }
      t =
    (p₀.trans p₁).toContinuousMap t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
t : ↑I
⊢ 0 ≤ 1 / 2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
t : ↑I
⊢ 1 / 2 ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x : ↑I × ↑I
⊢ 0 ≤ ↑(σ x.1)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x : ↑I × ↑I
⊢ 0 ≤ ↑x.1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x : ↑I × ↑I
⊢ ↑(σ x.1) + ↑x.1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ Continuous fun x ↦ p ⟨↑(σ x.1) * ↑x.2 + ↑x.1 * ↑(f x.2), ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x : ↑I
⊢ p ⟨↑(σ (0, x).1) * ↑(0, x).2 + ↑(0, x).1 * ↑(f (0, x).2), ⋯⟩ = p.toContinuousMap x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x : ↑I
⊢ p ⟨↑(σ (1, x).1) * ↑(1, x).2 + ↑(1, x).1 * ↑(f (1, x).2), ⋯⟩ = (p.reparam f hf hf₀ hf₁).toContinuousMap x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t x : ↑I
hx : x ∈ {0, 1}
⊢ { toFun := fun x ↦ p ⟨↑(σ (t, x).1) * ↑(t, x).2 + ↑(t, x).1 * ↑(f (t, x).2), ⋯⟩, continuous_toFun := ⋯ } x =
    p.toContinuousMap x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
⊢ ∀ (x : ↑I), F ((0, x).1, σ (0, x).2) = p.symm.toContinuousMap x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
⊢ ∀ (x : ↑I), F ((1, x).1, σ (1, x).2) = q.symm.toContinuousMap x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
⊢ ((p.map ⋯).trans (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
t x : ↑I
hx : x ∈ {0, 1}
⊢ { toFun := fun x ↦ F ((t, x).1, σ (t, x).2), continuous_toFun := ⋯ } x = p.symm.toContinuousMap x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
f : C(X, Y)
⊢ ∀ (x : ↑I), (⇑f ∘ ⇑F) (0, x) = (p.map ⋯).toContinuousMap x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
H : f.Homotopy g
⊢ ∀ ⦃X_1 Y_1 : FundamentalGroupoid X⦄ (f_1 : X_1 ⟶ Y_1),
    (map f).map f_1 ≫ ⟦H.evalAt Y_1.as⟧ = ⟦H.evalAt X_1.as⟧ ≫ (map g).map f_1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
f : C(X, Y)
⊢ ∀ (x : ↑I), (⇑f ∘ ⇑F) (1, x) = (q.map ⋯).toContinuousMap x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X✝ : Type u_1
Y✝ : Type u_2
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y✝
f g : C(X✝, Y✝)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hequiv : X ≃ₕ Y
⊢ ↑(π.obj (TopCat.of X)) ≌ ↑(π.obj (TopCat.of Y))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
⊢ SimplyConnectedSpace X ↔ Nonempty X ∧ ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : SimplyConnectedSpace X
x y : X
⊢ Nonempty (Unique (Path.Homotopic.Quotient x y))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ (π.map (TopCat.ofHom f)).map ⟦p⟧ ≍ (π.map (TopCat.ofHom g)).map ⟦q⟧

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
⊢ SimplyConnectedSpace Y → PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ f x₀ = g x₂

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
h : PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
⊢ SimplyConnectedSpace Y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ f x₁ = g x₃

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
f : C(X, Y)
t x : ↑I
hx : x ∈ {0, 1}
⊢ { toFun := fun x ↦ (⇑f ∘ ⇑F) (t, x), continuous_toFun := ⋯ } x = (p.map ⋯).toContinuousMap x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
⊢ SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p q : Path x₀ x₁
h : mk p = mk q
⊢ p.Homotopic q

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
Y : Type u_1
inst✝ : TopologicalSpace Y
x₀ y₀ : X
x₁ y₁ : Y
motive : Homotopic.Quotient x₀ y₀ → Homotopic.Quotient x₁ y₁ → Prop
mk : ∀ (a : Path x₀ y₀) (b : Path x₁ y₁), motive (Quotient.mk a) (Quotient.mk b)
q₀ : Homotopic.Quotient x₀ y₀
q₁ : Homotopic.Quotient x₁ y₁
⊢ motive q₀ q₁

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ (π.map (TopCat.ofHom f)).map ⟦p⟧ = hcast ⋯ ≫ (π.map (TopCat.ofHom g)).map ⟦q⟧ ≫ hcast ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Homotopic.Quotient x y
⊢ γ.cast ⋯ ⋯ = γ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Homotopic.Quotient x y
x' y' : X
hx : x' = x
hy : y' = y
x'' y'' : X
hx' : x'' = x'
hy' : y'' = y'
⊢ (γ.cast hx hy).cast hx' hy' = γ.cast ⋯ ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y x' y' : X
hx : x' = x
hy : y' = y
γ : Homotopic.Quotient x y
⊢ γ.cast hx hy ≍ γ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X
Z : Type u_1
inst✝ : TopologicalSpace Z
p : Homotopic.Quotient x₀ x₁
f : C(X, Y)
g : C(Y, Z)
⊢ p.map (g.comp f) = (p.map f).map g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
hpc : PathConnectedSpace Y
x y : Y
p₁ p₂ : Path x y
hloops : ∀ (x : Y) (γ : Path x x), ⟦γ⟧ = ⟦Path.refl x⟧
⊢ Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧) = Path.Homotopic.Quotient.refl x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
p : Homotopic.Quotient x y
x' y' : X
hx : x' = x
hy : y' = y
f : C(X, Y)
⊢ (p.cast hx hy).map f = (p.map f).cast ⋯ ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
hpc : PathConnectedSpace Y
x y : Y
p₁ p₂ : Path x y
hloops : ∀ (x : Y) (γ : Path x x), ⟦γ⟧ = ⟦Path.refl x⟧
h : Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧) = Path.Homotopic.Quotient.refl x
⊢ ⟦p₁⟧ = (Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧)).trans ⟦p₂⟧

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
⊢ (π.map (TopCat.ofHom f)).map ⟦p'⟧ =
    hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) ⟦p'⟧) ≫ hcast ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₂ x₃
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ x₀ = x₂

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
hpc : PathConnectedSpace Y
x y : Y
p₁ p₂ : Path x y
hloops : ∀ (x : Y) (γ : Path x x), ⟦γ⟧ = ⟦Path.refl x⟧
h : Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧) = Path.Homotopic.Quotient.refl x
⊢ (Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧)).trans ⟦p₂⟧ = ⟦p₂⟧

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₀ x₃
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ x₁ = x₃

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
⊢ SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X ≃ₜ Y
s : Set Y
⊢ IsSimplyConnected (⇑f ⁻¹' s) ↔ IsSimplyConnected s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₂ x₃
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ ⟦p₁⟧ ≍ ⟦p₂⟧

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
⊢ (π.map (TopCat.ofHom g)).map ⟦p'⟧ =
    hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) ⟦p'⟧) ≫ hcast ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X
inst✝ : Nonempty Y
⊢ (const Y x₀).Homotopic (const Y x₁) ↔ Joined x₀ x₁

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
⊢ ⟦H.evalAt x⟧ = hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x))) ≫ hcast ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : ↑s) (γ : Path x x), γ.Homotopic (Path.refl x)
x : X
p : Path x x
hp : ∀ (t : ↑unitInterval), p t ∈ s
⊢ x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : ↑s) (γ : Path x x), γ.Homotopic (Path.refl x)
x : { x // x ∈ s }
p : Path ↑x ↑x
hp : ∀ (t : ↑unitInterval), p t ∈ s
⊢ ⟨p 0, ⋯⟩ = x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : ↑s) (γ : Path x x), γ.Homotopic (Path.refl x)
x : { x // x ∈ s }
p : Path ↑x ↑x
hp : ∀ (t : ↑unitInterval), p t ∈ s
⊢ ⟨p 1, ⋯⟩ = x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : X) (p : Path x x), (∀ (t : ↑unitInterval), p t ∈ s) → ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
x : ↑s
p : Path x x
F : (p.map ⋯).Homotopy (Path.refl ↑x)
hF : ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
⊢ ∀ (x_1 : ↑unitInterval), ⟨F (0, x_1), ⋯⟩ = p.toContinuousMap x_1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : X) (p : Path x x), (∀ (t : ↑unitInterval), p t ∈ s) → ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
x : ↑s
p : Path x x
F : (p.map ⋯).Homotopy (Path.refl ↑x)
hF : ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
⊢ ∀ (x_1 : ↑unitInterval), ⟨F (1, x_1), ⋯⟩ = (Path.refl x).toContinuousMap x_1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : X) (p : Path x x), (∀ (t : ↑unitInterval), p t ∈ s) → ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
x : ↑s
p : Path x x
F : (p.map ⋯).Homotopy (Path.refl ↑x)
hF : ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
⊢ ∀ (t x_1 : ↑unitInterval),
    x_1 ∈ {0, 1} → { toFun := fun x_2 ↦ ⟨F (t, x_2), ⋯⟩, continuous_toFun := ⋯ } x_1 = p.toContinuousMap x_1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsSimplyConnected s ↔
    IsPathConnected s ∧
      ∀ (x : X) (p : Path x x), (∀ (t : ↑unitInterval), p t ∈ s) → ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: ⊢ Continuous fun x ↦ ↑x.2

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: ⊢ Continuous fun x ↦ 1 / 2

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: ⊢ ContinuousOn (fun x ↦ ↑x.1 * 2 * ↑x.2) {x | ↑x.2 ≤ 1 / 2}

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: ⊢ ContinuousOn (fun x ↦ ↑x.1 * (2 - 2 * ↑x.2)) {x | 1 / 2 ≤ ↑x.2}

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: ⊢ ∀ (x : ↑I × ↑I), ↑x.2 = 1 / 2 → ↑x.1 * 2 * ↑x.2 = ↑x.1 * (2 - 2 * ↑x.2)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
⊢ toHoCat.Full

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : ModelCategory C
X Y : CofibrantObject C
inst✝ : IsFibrant Y.obj
f g : X ⟶ Y
⊢ toHoCat.map f = toHoCat.map g ↔ homRel C f g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: x : ↑I × ↑I
⊢ reflTransSymmAux x ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ Continuous fun x ↦ p ⟨reflTransSymmAux x, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f g : X ⟶ Y
h : homRel C f g
⊢ weakEquivalences (CofibrantObject C) f ↔ weakEquivalences (CofibrantObject C) g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ ∀ (x : ↑I), p ⟨reflTransSymmAux (0, x), ⋯⟩ = (Path.refl x₀).toContinuousMap x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f : X ⟶ Y
⊢ WeakEquivalence (toHoCat.map f) ↔ WeakEquivalence f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
x✝² x✝¹ : CofibrantObject C
x✝ : x✝² ⟶ x✝¹
h : weakEquivalences (CofibrantObject C) x✝
⊢ (weakEquivalences (HoCat C)).inverseImage toHoCat x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w✝ : W s
f : T ⟶ Y
⊢ W s

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
hx : 2⁻¹ < ↑x
⊢ p.extend (2 - 2 * ↑x) = p.extend (1 - (2 * ↑x - 1))

Tactic:
by

Goal state after: