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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : t ≤ 0
x : X
⊢ (F.extend t) x = f₀ x

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : 1 ≤ t
x : X
⊢ (F.extend t) x = f₁ x

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ F.extend 0 = f₀

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ F.extend 1 = f₁

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : t ∈ I
x : X
⊢ (F.extend t) x = F (⟨t, ht⟩, x)

Tactic:
by

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ ∀ (x : X), F (σ (0, x).1, (0, x).2) = f₁ x

Tactic:
by

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ ∀ (x : X), F (σ (1, x).1, (1, x).2) = f₀ x

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ F.symm.symm = F

Tactic:
by

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
⊢ Continuous fun x ↦ ↑x.1

Tactic:
by

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
⊢ Continuous fun x ↦ (Set.projIcc 0 1 extend._proof_1 (2 * ↑x.1), x.2)

Tactic:
by

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
⊢ Continuous fun x ↦ (Set.projIcc 0 1 extend._proof_1 (2 * ↑x.1 - 1), x.2)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.EilenbergSteenrod

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Limits.HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
HP HP' : HomologyPretheory C c
f : HP ⟶ HP'
i : ι
⊢ (HP.iso i).hom ≫ incl.whiskerLeft (f.homₚ i) ≫ (HP'.iso i).inv = f.hom i

Tactic:
by

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
hx : ↑x.1 = 1 / 2
⊢ (F.extend (2 * ↑x.1)) x.2 = (G.extend (2 * ↑x.1 - 1)) x.2

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.EilenbergSteenrod

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Limits.HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
HP✝ HP'✝ HP HP' X✝¹ Y✝¹ : HomologyPretheory C c
e : X✝¹ ≅ Y✝¹
x✝¹ : isHomotopyInvariant C c X✝¹
X✝ Y✝ : TopPair
f✝ g✝ : X✝ ⟶ Y✝
F : Homotopy f✝ g✝
x✝ : ι
⊢ (Y✝¹.Hₚ x✝).map f✝ = (Y✝¹.Hₚ x✝).map g✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic

Goal state before:
pp: ⊢ ∀ {W X Y Z : Grpd} (f : ↑W ⥤ ↑X) (g : ↑X ⥤ ↑Y) (h : ↑Y ⥤ ↑Z), (f ⋙ g) ⋙ h = f ⋙ g ⋙ h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic

Goal state before:
pp: J : Type u
F : J → Grpd
⊢ ∀ (s : Limits.Fan F) (j : J), (Functor.pi' fun j ↦ s.proj j) ≫ (piLimitFan F).proj j = s.proj j

Tactic:
by

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : X
⊢ (if ↑(0, x).1 ≤ 1 / 2 then (F.extend (2 * ↑(0, x).1)) (0, x).2 else (G.extend (2 * ↑(0, x).1 - 1)) (0, x).2) = f₀ x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic

Goal state before:
pp: J : Type u
F : J → Grpd
⊢ ∀ (s : Limits.Fan F) (m : s.pt ⟶ (piLimitFan F).pt),
    (∀ (j : J), m ≫ (piLimitFan F).proj j = s.proj j) → m = Functor.pi' fun j ↦ s.proj j

Tactic:
intro s m w

Goal state after:
J : Type u
F : J → Grpd
s : Limits.Fan F
m : s.pt ⟶ (piLimitFan F).pt
w : ∀ (j : J), m ≫ (piLimitFan F).proj j = s.proj j
⊢ m = Functor.pi' fun j ↦ s.proj j
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : X
⊢ (if ↑(1, x).1 ≤ 1 / 2 then (F.extend (2 * ↑(1, x).1)) (1, x).2 else (G.extend (2 * ↑(1, x).1 - 1)) (1, x).2) = f₂ x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic

Goal state before:
pp: J : Type u
F : J → Grpd
⊢ ∀ (s : Limits.Fan F) (m : s.pt ⟶ (piLimitFan F).pt),
    (∀ (j : J), m ≫ (piLimitFan F).proj j = s.proj j) → m = Functor.pi' fun j ↦ s.proj j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic

Goal state before:
pp: ⊢ {J : Type u} → (f : J → Grpd) → Limits.Fan f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic

Goal state before:
pp: ⊢ {J : Type u} → (f : J → Grpd) → Limits.IsLimit (piLimitFan f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic

Goal state before:
pp: J : Type u
f : J → Grpd
j : J
⊢ (piIsoPi J f).hom ≫ Limits.Pi.π f j = Pi.eval (fun i ↦ ↑(f i)) j

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ ↑t = 1 / 2

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
⊢ (F.trans G).symm = G.symm.trans F.symm

Tactic:
by

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ g₀ g₁ : C(X, Y)
F : f₀.Homotopy f₁
h₀ : f₀ = g₀
h₁ : f₁ = g₁
⊢ ∀ (x : X), F (0, x) = g₀ x

Tactic:
by

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ g₀ g₁ : C(X, Y)
F : f₀.Homotopy f₁
h₀ : f₀ = g₀
h₁ : f₁ = g₁
⊢ ∀ (x : X), F (1, x) = g₁ x

Tactic:
by

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
g₀ g₁ : C(Y, Z)
G : g₀.Homotopy g₁
F : f₀.Homotopy f₁
⊢ ∀ (x : X), G ((0, x).1, F (0, x)) = (g₀.comp f₀) x

Tactic:
by

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
g₀ g₁ : C(Y, Z)
G : g₀.Homotopy g₁
F : f₀.Homotopy f₁
⊢ ∀ (x : X), G ((1, x).1, F (1, x)) = (g₁.comp f₁) x

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ ∀ {x y : C(X, Y)}, x.Homotopic y → y.Homotopic x

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ ∀ {x y z : C(X, Y)}, x.Homotopic y → y.Homotopic z → x.Homotopic z

Tactic:
by

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

Goal state before:
pp: F : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
P : C(X, Y) → Prop
toFun : ↑I × X → Y
continuous_toFun : Continuous toFun
toContinuousMap : C(↑I × X, Y) := { toFun := toFun, continuous_toFun := continuous_toFun }
map_zero_left : ∀ (x : X), toFun (0, x) = f₀ x
map_one_left : ∀ (x : X), toFun (1, x) = f₁ x
toHomotopy : f₀.Homotopy f₁ :=
  { toContinuousMap := toContinuousMap, map_zero_left := map_zero_left, map_one_left := map_one_left }
t : ↑I
⊢ Continuous (Prod.mk t)

Tactic:
by

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : f₀.HomotopyWith f₁ P
G : f₁.HomotopyWith f₂ P
t : ↑I
⊢ P { toFun := fun x ↦ (F.trans G.toHomotopy).toFun (t, x), continuous_toFun := ⋯ }

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
t : ↑I
x : X
hx : x ∈ S
⊢ F (t, x) = f₁ x

Tactic:
by

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
G : f₁.HomotopyRel f₂ S
t : ↑I
x : X
hx : x ∈ S
⊢ { toFun := fun x ↦ (F.trans G.toHomotopy).toFun (t, x), continuous_toFun := ⋯ } x = f₀ x

Tactic:
by

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
G : f₁.HomotopyRel f₂ S
t : ↑I
x : X
hx : x ∈ S
⊢ { toFun := fun x ↦ (F.trans G.toHomotopy).toFun (t, x), continuous_toFun := ⋯ } x = f₀ x

Tactic:
by
    simp only [Homotopy.trans]
    split_ifs
    · simp [HomotopyWith.extendProp F (2 * t) x hx, F.fst_eq_snd hx, G.fst_eq_snd hx]
    · simp [HomotopyWith.extendProp G (2 * t - 1) x hx, F.fst_eq_snd hx, G.fst_eq_snd hx]

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀✝ f₁✝ 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
x : X
hx : x ∈ S
⊢ { toFun := fun x ↦ (F.cast h₀ h₁).toFun (t, x), continuous_toFun := ⋯ } x = g₀ x

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set X
⊢ ∀ {x y : C(X, Y)}, x.HomotopicRel y S → y.HomotopicRel x S

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set X
⊢ ∀ {x y z : C(X, Y)}, x.HomotopicRel y S → y.HomotopicRel z S → x.HomotopicRel z S

Tactic:
by

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

Goal state before:
pp: I : Type u_1
A : Type u_2
X : I → Type u_3
inst✝¹ : (i : I) → TopologicalSpace (X i)
inst✝ : TopologicalSpace A
f g : (i : I) → C(A, X i)
S : Set A
homotopies : (i : I) → (f i).HomotopyRel (g i) S
⊢ ∀ (t : ↑unitInterval),
    ∀ x ∈ S,
      { toFun := fun x ↦ (Homotopy.pi fun i ↦ (homotopies i).toHomotopy).toFun (t, x), continuous_toFun := ⋯ } x =
        (ContinuousMap.pi f) x

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h : X ≃ₜ Y
⊢ ((↑h.symm).comp ↑h).Homotopic (ContinuousMap.id X)

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h : X ≃ₜ Y
⊢ ((↑h).comp ↑h.symm).Homotopic (ContinuousMap.id Y)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
A : Type u_3
inst✝ : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : f₀.Homotopy f₁
G : g₀.Homotopy g₁
x : A
⊢ (F (0, x), G (0, x)) = (f₀.prodMk g₀) x

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ ((h₁.invFun.comp h₂.invFun).comp (h₂.toFun.comp h₁.toFun)).Homotopic (ContinuousMap.id X)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
A : Type u_3
inst✝ : TopologicalSpace A
f₀ f₁ : C(A, α)
g₀ g₁ : C(A, β)
S : Set A
F : f₀.Homotopy f₁
G : g₀.Homotopy g₁
x : A
⊢ (F (1, x), G (1, x)) = (f₁.prodMk g₁) x

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ ((h₂.toFun.comp h₁.toFun).comp (h₁.invFun.comp h₂.invFun)).Homotopic (ContinuousMap.id Z)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
γ : (i : ι) → Path (as i) (bs i)
⊢ (pi fun i ↦ Quotient.mk (γ i)) = Quotient.mk (Path.pi γ)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)
⊢ pi γ₀ ⬝ pi γ₁ = pi fun i ↦ γ₀ i ⬝ γ₁ i

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
paths : (i : ι) → Homotopic.Quotient (as i) (bs i)
⊢ proj i (pi paths) = paths i

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
p : Homotopic.Quotient as bs
⊢ (pi fun i ↦ proj i p) = p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
⊢ prod q₁ q₂ ⬝ prod r₁ r₂ = prod (q₁ ⬝ r₁) (q₂ ⬝ r₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
⊢ projLeft (prod q₁ q₂) = q₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
⊢ projRight (prod q₁ q₂) = q₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)
⊢ prod (projLeft p) (projRight p) = p

Tactic:
by

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

Goal state before:
pp: I : Type u
X : I → TopCat
x : (i : I) → ↑(π.obj (X i))
⊢ Path.Homotopic.pi (𝟙 x) = 𝟙 { as := fun i ↦ (x i).as }

Tactic:
by

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

Goal state before:
pp: I : Type u
X : I → TopCat
⊢ piToPiTop X ≫ CategoryTheory.Functor.pi' (proj X) = 𝟙 (CategoryTheory.Grpd.of ((i : I) → ↑(π.obj (X i))))

Tactic:
by

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

Goal state before:
pp: I : Type u
X : I → TopCat
X✝ Y✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
f : X✝ ⟶ Y✝
this : Path.Homotopic.pi ((CategoryTheory.Functor.pi' (proj X)).map f) = f
⊢ (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).map f =
    CategoryTheory.eqToHom ⋯ ≫ (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).map f ≫ CategoryTheory.eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: I : Type u
X : I → TopCat
⊢ CategoryTheory.Functor.pi' (proj X) ≫ piToPiTop X = 𝟙 (π.obj (TopCat.of ((i : I) → ↑(X i))))

Tactic:
by

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

Goal state before:
pp: I : Type u
X : I → TopCat
⊢ Limits.PreservesLimit (Discrete.functor X) π

Tactic:
by

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

Goal state before:
pp: A : TopCat
B : TopCat
x₀ : ↑(π.obj A)
x₁ : ↑(π.obj B)
⊢ (match (x₀, x₁), (x₀, x₁), 𝟙 (x₀, x₁) with
    | (fst, snd), (fst_1, snd_1), (p₀, p₁) => Path.Homotopic.prod p₀ p₁) =
    𝟙 { as := ((x₀, x₁).1.as, (x₀, x₁).2.as) }

Tactic:
simp only

Goal state after:
A : TopCat
B : TopCat
x₀ : ↑(π.obj A)
x₁ : ↑(π.obj B)
⊢ (match (x₀, x₁), (x₀, x₁), 𝟙 (x₀, x₁) with
    | (fst, snd), (fst_1, snd_1), (p₀, p₁) => Path.Homotopic.prod p₀ p₁) =
    𝟙 { as := (x₀.as, x₁.as) }
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: A : TopCat
B : TopCat
⊢ ∀ (X : ↑(π.obj A) × ↑(π.obj B)),
    (match X, X, 𝟙 X with
      | (fst, snd), (fst_1, snd_1), (p₀, p₁) => Path.Homotopic.prod p₀ p₁) =
      𝟙 { as := (X.1.as, X.2.as) }

Tactic:
by

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

Goal state before:
pp: A : TopCat
B : TopCat
⊢ prodToProdTop A B ≫ (projLeft A B).prod' (projRight A B) = 𝟙 (CategoryTheory.Grpd.of (↑(π.obj A) × ↑(π.obj B)))

Tactic:
by

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

Goal state before:
pp: A : TopCat
B : TopCat
⊢ (projLeft A B).prod' (projRight A B) ≫ prodToProdTop A B = 𝟙 (π.obj (TopCat.of (↑A × ↑B)))

Tactic:
change (projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B = 𝟭 _

Goal state after:
A : TopCat
B : TopCat
⊢ (projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B = 𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: A : TopCat
B : TopCat
⊢ (projLeft A B).prod' (projRight A B) ≫ prodToProdTop A B = 𝟙 (π.obj (TopCat.of (↑A × ↑B)))

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₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : ↑I
⊢ (F.curry t) 0 = 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₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : ↑I
⊢ (F.curry t) 1 = x₁

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
⊢ F.eval 0 = 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₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
⊢ F.eval 1 = p₁

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₁
⊢ Continuous fun x ↦ (x.1, Set.projIcc 0 1 extend._proof_2 (2 * ↑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₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
⊢ Continuous fun x ↦ (x.1, Set.projIcc 0 1 extend._proof_2 (2 * ↑x.2 - 1))

Tactic:
by

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

Goal state before:
pp: x y : Path PUnit.unit PUnit.unit
⊢ x = y

Tactic:
by

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

Goal state before:
pp: x y : FundamentalGroupoid PUnit.{u_1 + 1}
⊢ Subsingleton (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 : ↑I × ↑I
hx : ↑x.2 = 1 / 2
⊢ (F.eval x.1).extend (2 * ↑x.2) = (G.eval x.1).extend (2 * ↑x.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₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : ↑I
⊢ (if ↑(0, x).2 ≤ 1 / 2 then (F.eval (0, x).1).extend (2 * ↑(0, x).2)
    else (G.eval (0, x).1).extend (2 * ↑(0, x).2 - 1)) =
    (p₀.trans 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₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : ↑I
⊢ (if ↑(1, x).2 ≤ 1 / 2 then (F.eval (1, x).1).extend (2 * ↑(1, x).2)
    else (G.eval (1, x).1).extend (2 * ↑(1, x).2 - 1)) =
    (q₀.trans q₁).toContinuousMap x

Tactic:
by

Goal state after: