mathlib-initiative/mathlib-tactics huggingface dataset:
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).IsStableUnderRetracts

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).IsStableUnderRetracts
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)
⊢ ((fibrations D).inverseImage e.functor).IsStableUnderRetracts

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)
⊢ ((fibrations D).inverseImage e.functor).IsStableUnderRetracts
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)
⊢ (fibrations C).IsStableUnderRetracts

Tactic:
by rw [h₂]; infer_instance

Goal state after:
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)
⊢ ((cofibrations D).inverseImage e.functor).IsStableUnderRetracts

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)
⊢ ((cofibrations D).inverseImage e.functor).IsStableUnderRetracts
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : FundamentalGroupoid X
f✝ : Path.Homotopic.Quotient X✝.as Y✝.as
f : Path X✝.as Y✝.as
⊢ Path.Homotopic.Quotient.trans ⟦Path.refl X✝.as⟧ (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f) =
    Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f

Tactic:
;

Goal state after:
case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : FundamentalGroupoid X
f✝ : Path.Homotopic.Quotient X✝.as Y✝.as
f : Path X✝.as Y✝.as
⊢ Path.Homotopic.Quotient.trans ⟦Path.refl X✝.as⟧ (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f) =
    Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : FundamentalGroupoid X
f✝ : Path.Homotopic.Quotient X✝.as Y✝.as
f : Path X✝.as Y✝.as
⊢ Path.Homotopic.Quotient.trans (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f) ⟦Path.refl Y✝.as⟧ =
    Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f

Tactic:
;

Goal state after:
case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : FundamentalGroupoid X
f✝ : Path.Homotopic.Quotient X✝.as Y✝.as
f : Path X✝.as Y✝.as
⊢ Path.Homotopic.Quotient.trans (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f) ⟦Path.refl Y✝.as⟧ =
    Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case mk.mk.mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
W✝ X✝ Y✝ Z✝ : FundamentalGroupoid X
f✝ : Path.Homotopic.Quotient W✝.as X✝.as
f : Path W✝.as X✝.as
g✝ : Path.Homotopic.Quotient X✝.as Y✝.as
g : Path X✝.as Y✝.as
h✝ : Path.Homotopic.Quotient Y✝.as Z✝.as
h : Path Y✝.as Z✝.as
⊢ (Path.Homotopic.Quotient.trans (Quot.mk (⇑(Path.Homotopic.setoid W✝.as X✝.as)) f)
          (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) g)).trans
      (Quot.mk (⇑(Path.Homotopic.setoid Y✝.as Z✝.as)) h) =
    Path.Homotopic.Quotient.trans (Quot.mk (⇑(Path.Homotopic.setoid W✝.as X✝.as)) f)
      (Path.Homotopic.Quotient.trans (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) g)
        (Quot.mk (⇑(Path.Homotopic.setoid Y✝.as Z✝.as)) h))

Tactic:
;

Goal state after:
case mk.mk.mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
W✝ X✝ Y✝ Z✝ : FundamentalGroupoid X
f✝ : Path.Homotopic.Quotient W✝.as X✝.as
f : Path W✝.as X✝.as
g✝ : Path.Homotopic.Quotient X✝.as Y✝.as
g : Path X✝.as Y✝.as
h✝ : Path.Homotopic.Quotient Y✝.as Z✝.as
h : Path Y✝.as Z✝.as
⊢ (Path.Homotopic.Quotient.trans (Quot.mk (⇑(Path.Homotopic.setoid W✝.as X✝.as)) f)
          (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) g)).trans
      (Quot.mk (⇑(Path.Homotopic.setoid Y✝.as Z✝.as)) h) =
    Path.Homotopic.Quotient.trans (Quot.mk (⇑(Path.Homotopic.setoid W✝.as X✝.as)) f)
      (Path.Homotopic.Quotient.trans (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) g)
        (Quot.mk (⇑(Path.Homotopic.setoid Y✝.as Z✝.as)) h))
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
X✝ Y✝ : FundamentalGroupoid X
a b : Path X✝.as Y✝.as
h : a.Homotopy b
⊢ ⟦a.symm⟧ = ⟦b.symm⟧

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : FundamentalGroupoid X
a b : Path X✝.as Y✝.as
h : a.Homotopy b
⊢ ⟦a.symm⟧ = ⟦b.symm⟧
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)
⊢ ((trivialCofibrations D).inverseImage e.functor).HasFactorization ((fibrations D).inverseImage e.functor)

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)
⊢ ((trivialCofibrations D).inverseImage e.functor).HasFactorization ((fibrations D).inverseImage e.functor)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : FundamentalGroupoid X
f✝ : Path.Homotopic.Quotient X✝.as Y✝.as
f : Path X✝.as Y✝.as
⊢ (Quotient.lift (fun f ↦ ⟦f.symm⟧) ⋯ (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f)).trans
      (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f) =
    ⟦Path.refl Y✝.as⟧

Tactic:
;

Goal state after:
case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : FundamentalGroupoid X
f✝ : Path.Homotopic.Quotient X✝.as Y✝.as
f : Path X✝.as Y✝.as
⊢ (Quotient.lift (fun f ↦ ⟦f.symm⟧) ⋯ (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f)).trans
      (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f) =
    ⟦Path.refl Y✝.as⟧
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : FundamentalGroupoid X
f✝ : Path.Homotopic.Quotient X✝.as Y✝.as
f : Path X✝.as Y✝.as
⊢ Path.Homotopic.Quotient.trans (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f)
      (Quotient.lift (fun f ↦ ⟦f.symm⟧) ⋯ (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f)) =
    ⟦Path.refl X✝.as⟧

Tactic:
;

Goal state after:
case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : FundamentalGroupoid X
f✝ : Path.Homotopic.Quotient X✝.as Y✝.as
f : Path X✝.as Y✝.as
⊢ Path.Homotopic.Quotient.trans (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f)
      (Quotient.lift (fun f ↦ ⟦f.symm⟧) ⋯ (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f)) =
    ⟦Path.refl X✝.as⟧
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case mk.mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
f : C(X, Y)
X✝ Y✝ Z✝ : FundamentalGroupoid X
f✝ : X✝ ⟶ Y✝
p : Path X✝.as Y✝.as
g✝ : Y✝ ⟶ Z✝
q : Path Y✝.as Z✝.as
⊢ Path.Homotopic.Quotient.map
      (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) p ≫ Quot.mk (⇑(Path.Homotopic.setoid Y✝.as Z✝.as)) q) f =
    Path.Homotopic.Quotient.map (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) p) f ≫
      Path.Homotopic.Quotient.map (Quot.mk (⇑(Path.Homotopic.setoid Y✝.as Z✝.as)) q) f

Tactic:
;

Goal state after:
case mk.mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
f : C(X, Y)
X✝ Y✝ Z✝ : FundamentalGroupoid X
f✝ : X✝ ⟶ Y✝
p : Path X✝.as Y✝.as
g✝ : Y✝ ⟶ Z✝
q : Path Y✝.as Z✝.as
⊢ Path.Homotopic.Quotient.map
      (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) p ≫ Quot.mk (⇑(Path.Homotopic.setoid Y✝.as Z✝.as)) q) f =
    Path.Homotopic.Quotient.map (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) p) f ≫
      Path.Homotopic.Quotient.map (Quot.mk (⇑(Path.Homotopic.setoid Y✝.as Z✝.as)) q) f
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)
⊢ ((cofibrations D).inverseImage e.functor).HasFactorization ((trivialFibrations D).inverseImage e.functor)

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)
⊢ ((cofibrations D).inverseImage e.functor).HasFactorization ((trivialFibrations D).inverseImage e.functor)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ { obj := fun x ↦ { as := (ContinuousMap.id X) x.as },
      map := fun {X_1 Y} p ↦ Path.Homotopic.Quotient.map p (ContinuousMap.id X), map_id := ⋯, map_comp := ⋯ } =
    𝟭 (FundamentalGroupoid X)

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ { obj := fun x ↦ { as := (ContinuousMap.id X) x.as },
      map := fun {X_1 Y} p ↦ Path.Homotopic.Quotient.map p (ContinuousMap.id X), map_id := ⋯, map_comp := ⋯ } =
    𝟭 (FundamentalGroupoid X)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ (fun {X_1 Y} p ↦ Path.Homotopic.Quotient.map p (ContinuousMap.id X)) = fun {X_1 Y} f ↦ f

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (fun {X_1 Y} p ↦ Path.Homotopic.Quotient.map p (ContinuousMap.id X)) = fun {X_1 Y} f ↦ f
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case mk
X : Type u_1
inst✝ : TopologicalSpace X
x y : FundamentalGroupoid X
x✝ : x ⟶ y
p : Path x.as y.as
⊢ Path.Homotopic.Quotient.map (Quot.mk (⇑(Path.Homotopic.setoid x.as y.as)) p) (ContinuousMap.id X) =
    Quot.mk (⇑(Path.Homotopic.setoid x.as y.as)) p

Tactic:
;

Goal state after:
case mk
X : Type u_1
inst✝ : TopologicalSpace X
x y : FundamentalGroupoid X
x✝ : x ⟶ y
p : Path x.as y.as
⊢ Path.Homotopic.Quotient.map (Quot.mk (⇑(Path.Homotopic.setoid x.as y.as)) p) (ContinuousMap.id X) =
    Quot.mk (⇑(Path.Homotopic.setoid x.as y.as)) p
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
Z : Type u_3
inst✝ : TopologicalSpace Z
g : C(Y, Z)
f : C(X, Y)
⊢ { obj := fun x ↦ { as := (g.comp f) x.as }, map := fun {X_1 Y_1} p ↦ Path.Homotopic.Quotient.map p (g.comp f),
      map_id := ⋯, map_comp := ⋯ } =
    { obj := fun x ↦ { as := f x.as }, map := fun {X_1 Y_1} p ↦ Path.Homotopic.Quotient.map p f, map_id := ⋯,
        map_comp := ⋯ } ⋙
      { obj := fun x ↦ { as := g x.as }, map := fun {X Y_1} p ↦ Path.Homotopic.Quotient.map p g, map_id := ⋯,
        map_comp := ⋯ }

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
Z : Type u_3
inst✝ : TopologicalSpace Z
g : C(Y, Z)
f : C(X, Y)
⊢ { obj := fun x ↦ { as := (g.comp f) x.as }, map := fun {X_1 Y_1} p ↦ Path.Homotopic.Quotient.map p (g.comp f),
      map_id := ⋯, map_comp := ⋯ } =
    { obj := fun x ↦ { as := f x.as }, map := fun {X_1 Y_1} p ↦ Path.Homotopic.Quotient.map p f, map_id := ⋯,
        map_comp := ⋯ } ⋙
      { obj := fun x ↦ { as := g x.as }, map := fun {X Y_1} p ↦ Path.Homotopic.Quotient.map p g, map_id := ⋯,
        map_comp := ⋯ }
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
Z : Type u_3
inst✝ : TopologicalSpace Z
g : C(Y, Z)
f : C(X, Y)
⊢ (fun {X_1 Y_1} p ↦ Path.Homotopic.Quotient.map p (g.comp f)) = fun {X_1 Y_1} f_1 ↦
    { obj := fun x ↦ { as := g x.as }, map := fun {X Y_2} p ↦ Path.Homotopic.Quotient.map p g, map_id := ⋯,
          map_comp := ⋯ }.map
      ({ obj := fun x ↦ { as := f x.as }, map := fun {X_2 Y_2} p ↦ Path.Homotopic.Quotient.map p f, map_id := ⋯,
            map_comp := ⋯ }.map
        f_1)

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
Z : Type u_3
inst✝ : TopologicalSpace Z
g : C(Y, Z)
f : C(X, Y)
⊢ (fun {X_1 Y_1} p ↦ Path.Homotopic.Quotient.map p (g.comp f)) = fun {X_1 Y_1} f_1 ↦
    { obj := fun x ↦ { as := g x.as }, map := fun {X Y_2} p ↦ Path.Homotopic.Quotient.map p g, map_id := ⋯,
          map_comp := ⋯ }.map
      ({ obj := fun x ↦ { as := f x.as }, map := fun {X_2 Y_2} p ↦ Path.Homotopic.Quotient.map p f, map_id := ⋯,
            map_comp := ⋯ }.map
        f_1)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case mk
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
Z : Type u_3
inst✝ : TopologicalSpace Z
g : C(Y, Z)
f : C(X, Y)
x y : FundamentalGroupoid X
x✝ : x ⟶ y
p : Path x.as y.as
⊢ Path.Homotopic.Quotient.map (Quot.mk (⇑(Path.Homotopic.setoid x.as y.as)) p) (g.comp f) =
    { obj := fun x ↦ { as := g x.as }, map := fun {X Y_1} p ↦ Path.Homotopic.Quotient.map p g, map_id := ⋯,
          map_comp := ⋯ }.map
      ({ obj := fun x ↦ { as := f x.as }, map := fun {X_1 Y_1} p ↦ Path.Homotopic.Quotient.map p f, map_id := ⋯,
            map_comp := ⋯ }.map
        (Quot.mk (⇑(Path.Homotopic.setoid x.as y.as)) p))

Tactic:
;

Goal state after:
case mk
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
Z : Type u_3
inst✝ : TopologicalSpace Z
g : C(Y, Z)
f : C(X, Y)
x y : FundamentalGroupoid X
x✝ : x ⟶ y
p : Path x.as y.as
⊢ Path.Homotopic.Quotient.map (Quot.mk (⇑(Path.Homotopic.setoid x.as y.as)) p) (g.comp f) =
    { obj := fun x ↦ { as := g x.as }, map := fun {X Y_1} p ↦ Path.Homotopic.Quotient.map p g, map_id := ⋯,
          map_comp := ⋯ }.map
      ({ obj := fun x ↦ { as := f x.as }, map := fun {X_1 Y_1} p ↦ Path.Homotopic.Quotient.map p f, map_id := ⋯,
            map_comp := ⋯ }.map
        (Quot.mk (⇑(Path.Homotopic.setoid x.as y.as)) p))
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x₀ : X
⊢ eqToHom ⋯ = (Path.Homotopic.Quotient.refl x₀).cast ⋯ ⋯

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x₀ : X
⊢ eqToHom ⋯ = (Path.Homotopic.Quotient.refl x₀).cast ⋯ ⋯
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x' y' : X
p : Path.Homotopic.Quotient x' y'
⊢ eqToHom ⋯ ≫ p ≫ eqToHom ⋯ = p.cast ⋯ ⋯

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x' y' : X
p : Path.Homotopic.Quotient x' y'
⊢ eqToHom ⋯ ≫ p ≫ eqToHom ⋯ = p.cast ⋯ ⋯
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

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
J : MulticospanShape
d : MulticospanIndex J C
c : Multifork d
F : C ⥤ D
i : J.L
⊢ (Iso.refl ((Cone.postcompose (d.multicospanMapIso F).inv).obj (F.mapCone c)).pt).hom ≫
      (c.map F).π.app (WalkingMulticospan.left i) =
    ((Cone.postcompose (d.multicospanMapIso F).inv).obj (F.mapCone c)).π.app (WalkingMulticospan.left i)

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
J : MulticospanShape
d : MulticospanIndex J C
c : Multifork d
F : C ⥤ D
i : J.L
⊢ (Iso.refl ((Cone.postcompose (d.multicospanMapIso F).inv).obj (F.mapCone c)).pt).hom ≫
      (c.map F).π.app (WalkingMulticospan.left i) =
    ((Cone.postcompose (d.multicospanMapIso F).inv).obj (F.mapCone c)).π.app (WalkingMulticospan.left i)