mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.Ordered

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
x✝ : α
⊢ (s.inf' H f) x✝ = s.inf' H (fun i ↦ ⇑(f i)) x✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
x✝ : α
⊢ (s.inf' H f) x✝ = s.inf' H (fun i ↦ ⇑(f i)) x✝
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
A : IndexSet (op ⦋i⦌)
a✝ : A ∈ Finset.univ
hA : A ≠ IndexSet.id (op ⦋i⦌)
⊢ ((s.πSummand A ≫ (s.cofan (op ⦋i⦌)).inj A) ≫ K[X].d i j) ≫ s.πSummand (IndexSet.id (op ⦋j⦌)) = 0

Tactic:
simp only [assoc, s.ιSummand_comp_d_comp_πSummand_eq_zero _ _ _ hA, comp_zero]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.SingleObj

Goal state before:
pp: case cons
α : Type u_1
x b✝ c✝ : SingleObj α
a✝¹ : Path (star α) b✝
a✝ : b✝ ⟶ c✝
ih : listToPath (pathToList a✝¹) = a✝¹
⊢ (listToPath (pathToList a✝¹)).cons a✝ = a✝¹.cons a✝

Tactic:
;

Goal state after:
case cons
α : Type u_1
x b✝ c✝ : SingleObj α
a✝¹ : Path (star α) b✝
a✝ : b✝ ⟶ c✝
ih : listToPath (pathToList a✝¹) = a✝¹
⊢ (listToPath (pathToList a✝¹)).cons a✝ = a✝¹.cons a✝
Module: Mathlib.Combinatorics.Quiver.SingleObj

Goal state before:
pp: case cons
α : Type u_1
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ a :: pathToList (listToPath l) = a :: l

Tactic:
;

Goal state after:
case cons
α : Type u_1
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ a :: pathToList (listToPath l) = a :: l
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X✝¹ Y✝¹ X Y Z : TopPair
X✝ Y✝ : TopCat
f : X✝ ⟶ Y✝
x : ↑snd
⊢ (ConcreteCategory.hom (𝟙 snd ≫ map)) x = (ConcreteCategory.hom (map ≫ f)) x

Tactic:
;

Goal state after:
X✝¹ Y✝¹ X Y Z : TopPair
X✝ Y✝ : TopCat
f : X✝ ⟶ Y✝
x : ↑snd
⊢ (ConcreteCategory.hom (𝟙 snd ≫ map)) x = (ConcreteCategory.hom (map ≫ f)) x
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₁
a✝ : X
⊢ (F.curry 0) a✝ = f₀ a✝

Tactic:
;

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
a✝ : X
⊢ (F.curry 0) a✝ = f₀ a✝
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₁
a✝ : X
⊢ (F.curry 1) a✝ = f₁ a✝

Tactic:
;

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
a✝ : X
⊢ (F.curry 1) a✝ = f₁ a✝
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:
;

Goal state after:
W✝ X✝ Y✝ Z✝ : Grpd
f✝ : ↑W✝ ⥤ ↑X✝
g✝ : ↑X✝ ⥤ ↑Y✝
h✝ : ↑Y✝ ⥤ ↑Z✝
⊢ (f✝ ⋙ g✝) ⋙ h✝ = f✝ ⋙ g✝ ⋙ h✝
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
w : ∀ (j : J), m ≫ (piLimitFan F).proj j = s.proj j
j : J
⊢ m ⋙ Pi.eval (fun i ↦ ↑(F i)) j = (Functor.pi' fun j ↦ s.proj j) ⋙ Pi.eval (fun i ↦ ↑(F i)) j

Tactic:
;

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
j : J
⊢ m ⋙ Pi.eval (fun i ↦ ↑(F i)) j = (Functor.pi' fun j ↦ s.proj j) ⋙ Pi.eval (fun i ↦ ↑(F i)) j
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
  induction paths using Quotient.induction_on_pi
  simp only [Quotient.mk''_eq_mk]
  rw [proj, pi_lift]
  congr

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

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

Tactic:
;

Goal state after:
I : Type u
X : I → TopCat
X✝ : (i : I) → ↑(π.obj (X i))
⊢ (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X✝ = (𝟭 ((i : I) → ↑(π.obj (X i)))).obj X✝
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

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

Tactic:
;

Goal state after:
I : Type u
X : I → TopCat
X✝ Y✝ : (i : I) → ↑(π.obj (X i))
f✝ : X✝ ⟶ Y✝
⊢ (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).map f✝ =
    CategoryTheory.eqToHom ⋯ ≫ (𝟭 ((i : I) → ↑(π.obj (X i)))).map f✝ ≫ CategoryTheory.eqToHom ⋯
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

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

Tactic:
;

Goal state after:
I : Type u
X : I → TopCat
X✝ Y✝ : (i : I) → ↑(π.obj (X i))
f✝ : X✝ ⟶ Y✝
i✝ : I
⊢ (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).map f✝ i✝ =
    (CategoryTheory.eqToHom ⋯ ≫ (𝟭 ((i : I) → ↑(π.obj (X i)))).map f✝ ≫ CategoryTheory.eqToHom ⋯) i✝
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: case h_obj
I : Type u
X : I → TopCat
X✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
⊢ (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).obj X✝ = (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).obj X✝

Tactic:
;

Goal state after:
case h_obj
I : Type u
X : I → TopCat
X✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
⊢ (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).obj X✝ = (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).obj X✝
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: case h_obj
A : TopCat
B : TopCat
⊢ ∀ (X : ↑(π.obj A) × ↑(π.obj B)),
    (prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X = (𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X

pp: case h_map
A : TopCat
B : TopCat
⊢ ∀ (X Y : ↑(π.obj A) × ↑(π.obj B)) (f : X ⟶ Y),
    (prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).map f ≍ (𝟭 (↑(π.obj A) × ↑(π.obj B))).map f

Tactic:
;

Goal state after:
case h_obj
A : TopCat
B : TopCat
⊢ ∀ (X : ↑(π.obj A) × ↑(π.obj B)),
    (prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X = (𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X

case h_map
A : TopCat
B : TopCat
⊢ ∀ (X Y : ↑(π.obj A) × ↑(π.obj B)) (f : X ⟶ Y),
    (prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).map f ≍ (𝟭 (↑(π.obj A) × ↑(π.obj B))).map f
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: case h_obj
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X✝ = (𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X✝

Tactic:
;

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

Goal state before:
pp: case h_obj
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ ((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X✝ = (𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝

Tactic:
;

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

Goal state before:
pp: case h_obj
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X✝).as =
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝).as

Tactic:
;

Goal state after:
case h_obj
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X✝).as =
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝).as
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
p : X
h : (ContinuousMap.id X).Homotopy (const X p)
this : ∀ (x : X), Joined p x
⊢ ∃ x, pathComponent x = Set.univ

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : (ContinuousMap.id X).Homotopy (const X p)
this : ∀ (x : X), Joined p x
⊢ ∃ x, pathComponent x = Set.univ
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: case h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : (ContinuousMap.id X).Homotopy (const X p)
this : ∀ (x : X), Joined p x
⊢ pathComponent p = Set.univ

Tactic:
;

Goal state after:
case h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : (ContinuousMap.id X).Homotopy (const X p)
this : ∀ (x : X), Joined p x
⊢ pathComponent p = Set.univ
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: case h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : (ContinuousMap.id X).Homotopy (const X p)
this : ∀ (x : X), Joined p x
x✝ : X
⊢ x✝ ∈ pathComponent p ↔ x✝ ∈ Set.univ

Tactic:
;

Goal state after:
case h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : (ContinuousMap.id X).Homotopy (const X p)
this : ∀ (x : X), Joined p x
x✝ : X
⊢ x✝ ∈ pathComponent p ↔ x✝ ∈ Set.univ
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✝ : Nonempty X ∧ ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))
x y : X
⊢ Nonempty (Unique (Path.Homotopic.Quotient x y))

Tactic:
;

Goal state after:
X✝ : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty X ∧ ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))
x y : X
⊢ Nonempty (Unique (Path.Homotopic.Quotient x y))
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

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

Tactic:
;

Goal state after:
Y : Type u_2
inst✝ : TopologicalSpace Y
a✝ : SimplyConnectedSpace Y
⊢ PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

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

Tactic:
;

Goal state after:
case intro
Y : Type u_2
inst✝ : TopologicalSpace Y
left✝ : PathConnectedSpace Y
right✝ : ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
⊢ SimplyConnectedSpace Y
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
a✝¹ a✝ : Y
⊢ (∀ (p₁ p₂ : Path a✝¹ a✝), p₁.Homotopic p₂) ↔ ∀ (x y : Path a✝¹ a✝), (Path.Homotopic.setoid a✝¹ a✝) x y

Tactic:
;

Goal state after:
Y : Type u_2
inst✝ : TopologicalSpace Y
a✝¹ a✝ : Y
⊢ (∀ (p₁ p₂ : Path a✝¹ a✝), p₁.Homotopic p₂) ↔ ∀ (x y : Path a✝¹ a✝), (Path.Homotopic.setoid a✝¹ a✝) x y
Module: Mathlib.Topology.Homotopy.Path

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

Tactic:
;

Goal state after:
case refl
X : Type u
inst✝ : TopologicalSpace X
x y y' : X
hy : y' = y
γ : Homotopic.Quotient x y
⊢ γ.cast ⋯ hy ≍ γ
Module: Mathlib.Topology.Homotopy.Path

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

Tactic:
;

Goal state after:
case refl.refl
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Homotopic.Quotient x y
⊢ γ.cast ⋯ ⋯ ≍ γ
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: case mk
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)
a✝ : Path x₀ x₁
⊢ map (Quot.mk (⇑(Homotopic.setoid x₀ x₁)) a✝) (g.comp f) = (map (Quot.mk (⇑(Homotopic.setoid x₀ x₁)) a✝) f).map g

Tactic:
;

Goal state after:
case mk
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)
a✝ : Path x₀ x₁
⊢ map (Quot.mk (⇑(Homotopic.setoid x₀ x₁)) a✝) (g.comp f) = (map (Quot.mk (⇑(Homotopic.setoid x₀ x₁)) a✝) f).map g
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: case mk
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)
a✝ : Path x y
⊢ (cast (Quot.mk (⇑(Homotopic.setoid x y)) a✝) hx hy).map f = (map (Quot.mk (⇑(Homotopic.setoid x y)) a✝) f).cast ⋯ ⋯

Tactic:
;

Goal state after:
case mk
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)
a✝ : Path x y
⊢ (cast (Quot.mk (⇑(Homotopic.setoid x y)) a✝) hx hy).map f = (map (Quot.mk (⇑(Homotopic.setoid x y)) a✝) f).cast ⋯ ⋯
Module: Mathlib.Topology.Homotopy.Path

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

Tactic:
;

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ ⟦p₁⟧ = ⟦p₂⟧
Module: Mathlib.Topology.Homotopy.Path

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

Tactic:
;

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ p₁ = p₂
Module: Mathlib.Topology.Homotopy.Path

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

Tactic:
;

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : ↑I), p₁ t = p₂ t
t : ↑I
⊢ p₁ t = p₂ t
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
⊢ ∀ (t : ↑I), (H.evalAt x) t = ((fun q ↦ q.map ⋯) (unitInterval.upath01.prod (Path.refl (fromTop x).as))) t

Tactic:
;

Goal state after:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
⊢ ∀ (t : ↑I), (H.evalAt x) t = ((fun q ↦ q.map ⋯) (unitInterval.upath01.prod (Path.refl (fromTop x).as))) t
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
t✝ : ↑I
⊢ (H.evalAt x) t✝ = ((fun q ↦ q.map ⋯) (unitInterval.upath01.prod (Path.refl (fromTop x).as))) t✝

Tactic:
;

Goal state after:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
t✝ : ↑I
⊢ (H.evalAt x) t✝ = ((fun q ↦ q.map ⋯) (unitInterval.upath01.prod (Path.refl (fromTop x).as))) t✝
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
⊢ (Quotient.functor (homRel C)).Full

Tactic:
;

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
⊢ (Quotient.functor (homRel C)).Full
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:
dsimp [toHoCat]
  rw [← Functor.homRel_iff, Quotient.functor_homRel_eq_compClosure_eqvGen,
    HomRel.compClosure_eq_self, homRel_equivalence_of_isFibrant_tgt.eqvGen_eq]

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 : CofibrantObject C
⊢ IsCofibrant X.obj

Tactic:
;

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ IsCofibrant X.obj
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
⊢ (Quotient.functor (homRel C)).Full

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
⊢ (Quotient.functor (homRel C)).Full
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f g : X ⟶ Y
⊢ RightHomotopyRel f g ↔ L.map f = L.map g

Tactic:
refine ⟨fun h ↦ (RightHomotopyRel.factorsThroughLocalization C h).map_eq L,
    fun h ↦ ?_⟩

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f g : X ⟶ Y
h : L.map f = L.map g
⊢ RightHomotopyRel f g
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: case mk
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsCofibrant Y
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
x✝ : RightHomotopyClass X Y
f : X ⟶ Y
⊢ Quot.lift (fun f ↦ RightHomotopyClass.mk f.hom) ⋯
      (Quot.lift (fun f ↦ toHoCat.map (homMk f)) ⋯ (Quot.mk RightHomotopyRel f)) =
    Quot.mk RightHomotopyRel f

Tactic:
;

Goal state after:
case mk
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsCofibrant Y
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
x✝ : RightHomotopyClass X Y
f : X ⟶ Y
⊢ Quot.lift (fun f ↦ RightHomotopyClass.mk f.hom) ⋯
      (Quot.lift (fun f ↦ toHoCat.map (homMk f)) ⋯ (Quot.mk RightHomotopyRel f)) =
    Quot.mk RightHomotopyRel f
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: case mk
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsCofibrant Y
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
x✝ : toHoCat.obj (mk X) ⟶ toHoCat.obj (mk Y)
f : (toHoCat.obj (mk X)).as ⟶ (toHoCat.obj (mk Y)).as
⊢ Quot.lift (fun f ↦ toHoCat.map (homMk f)) ⋯
      (Quot.lift (fun f ↦ RightHomotopyClass.mk f.hom) ⋯ (Quot.mk (HomRel.CompClosure (homRel C)) f)) =
    Quot.mk (HomRel.CompClosure (homRel C)) f

Tactic:
;

Goal state after:
case mk
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsCofibrant Y
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
x✝ : toHoCat.obj (mk X) ⟶ toHoCat.obj (mk Y)
f : (toHoCat.obj (mk X)).as ⟶ (toHoCat.obj (mk Y)).as
⊢ Quot.lift (fun f ↦ toHoCat.map (homMk f)) ⋯
      (Quot.lift (fun f ↦ RightHomotopyClass.mk f.hom) ⋯ (Quot.mk (HomRel.CompClosure (homRel C)) f)) =
    Quot.mk (HomRel.CompClosure (homRel C)) f
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ (weakEquivalences (Over S)).IsStableUnderRetracts

Tactic:
by
  rw [weakEquivalences_over_def, MorphismProperty.over_eq_inverseImage]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).HasTwoOutOfThreeProperty
⊢ (weakEquivalences (Over S)).HasTwoOutOfThreeProperty

Tactic:
by
  rw [weakEquivalences_over_def, MorphismProperty.over_eq_inverseImage]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : C
w✝ : IsCofibrant X
⊢ bifibrantResolution.map (adjUnit.app (toHoCat.obj (mk X))) =
    inv (adjCounitIso.hom.app (bifibrantResolution.obj (toHoCat.obj (mk X))))

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : C
w✝ : IsCofibrant X
⊢ bifibrantResolution.map (adjUnit.app (toHoCat.obj (mk X))) =
    inv (adjCounitIso.hom.app (bifibrantResolution.obj (toHoCat.obj (mk X))))
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : BifibrantObject C
⊢ adjUnit.app (BifibrantObject.HoCat.ιCofibrantObject.obj (BifibrantObject.toHoCat.obj X)) =
    inv (BifibrantObject.HoCat.ιCofibrantObject.map (adjCounitIso.hom.app (BifibrantObject.toHoCat.obj X)))

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : BifibrantObject C
⊢ adjUnit.app (BifibrantObject.HoCat.ιCofibrantObject.obj (BifibrantObject.toHoCat.obj X)) =
    inv (BifibrantObject.HoCat.ιCofibrantObject.map (adjCounitIso.hom.app (BifibrantObject.toHoCat.obj X)))
Module: Mathlib.AlgebraicTopology.ModelCategory.Transport

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor
h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this✝ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ ((weakEquivalences D).inverseImage e.functor).HasTwoOutOfThreeProperty

Tactic:
;

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor
h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this✝ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ ((weakEquivalences D).inverseImage e.functor).HasTwoOutOfThreeProperty