mathlib-initiative/mathlib-tactics huggingface dataset:
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
  induction p using Quotient.inductionOn
  simp only [Quotient.mk''_eq_mk, ← Path.Homotopic.Quotient.mk_map, pi_lift]
  congr

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
    change CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X = 𝟭 _
    apply CategoryTheory.Functor.ext
    · intro _ _ f
      suffices Path.Homotopic.pi ((CategoryTheory.Functor.pi' (proj X)).map f) = f by simpa
      change Path.Homotopic.pi (fun i => (CategoryTheory.Functor.pi' (proj X)).map f i) = _
      simp
    · intros; rfl

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

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

Tactic:
intro

Goal state after:
case mp
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝ : ContractibleSpace Y
⊢ (ContinuousMap.id Y).Nullhomotopic
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
  rcases ContractibleSpace.hequiv_unit' (X := X) with ⟨h⟩
  rcases ContractibleSpace.hequiv_unit' (X := Y) with ⟨h'⟩
  exact ⟨h.trans h'.symm⟩

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:
intro

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 left
Y : Type u_2
inst✝ : TopologicalSpace Y
a✝ : SimplyConnectedSpace Y
⊢ PathConnectedSpace Y

Tactic:
infer_instance

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

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

Tactic:
infer_instance

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

Goal state before:
pp: case mk
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₁
a : Path x₀ y₀
⊢ motive (Quot.mk (⇑(Homotopic.setoid x₀ y₀)) a) q₁

Tactic:
induction q₁ using Quot.ind with

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
⊢ ∀ (t : ↑I), (H.evalAt x) t = ((fun q ↦ q.map ⋯) (unitInterval.upath01.prod (Path.refl (fromTop x).as))) t

Tactic:
intro

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:
infer_instance

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
P : PathObject Y.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject C ⥤ (weakEquivalences (CofibrantObject C)).Localization := (weakEquivalences (CofibrantObject C)).Q
⊢ WeakEquivalence P.ι

Tactic:
infer_instance

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 : C
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (initial.to X)
⊢ Cofibration h.i

Tactic:
infer_instance

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₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : G ⊣ F
⊢ ((isomorphisms C₂).inverseImage G).functorCategory C₁ adj.unit

Tactic:
intro

Goal state after:
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₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : G ⊣ F
j✝ : C₁
⊢ (isomorphisms C₂).inverseImage G (adj.unit.app j✝)
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₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : G ⊣ F
j✝ : C₁
⊢ IsIso (G.map (adj.unit.app j✝))

Tactic:
infer_instance

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₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : F ⊣ G
⊢ ((isomorphisms C₂).inverseImage G).functorCategory C₁ adj.counit

Tactic:
intro

Goal state after:
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₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : F ⊣ G
j✝ : C₁
⊢ (isomorphisms C₂).inverseImage G (adj.counit.app j✝)
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₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : F ⊣ G
j✝ : C₁
⊢ IsIso (G.map (adj.counit.app j✝))

Tactic:
infer_instance

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
⊢ WeakEquivalence { hom := HoCat.pResolutionObj X.obj }.hom

Tactic:
infer_instance

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
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : HoCat C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences (HoCat C))
X : CofibrantObject C
⊢ WeakEquivalence (HoCat.ιCompResolutionNatTrans.app X)

Tactic:
infer_instance

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
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences C)
X : C
⊢ WeakEquivalence (HoCat.pResolutionObj X)

Tactic:
infer_instance

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:
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
⊢ (Quotient.functor (homRel C)).Full

Tactic:
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
inst✝ : LocallySmall.{w, v, u} C
⊢ LocallySmall.{w, v, u} (CategoryTheory.Quotient (homRel C))

Tactic:
infer_instance

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

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

Tactic:
infer_instance

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

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

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (cofibrations C).IsStableUnderRetracts
⊢ (fibrations Cᵒᵖ).IsStableUnderRetracts

Tactic:
rw [fibrations_op]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (cofibrations C).IsStableUnderRetracts
⊢ (cofibrations C).op.IsStableUnderRetracts
Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (cofibrations C).IsStableUnderRetracts
⊢ (cofibrations C).op.IsStableUnderRetracts

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (fibrations C).IsStableUnderRetracts
⊢ (fibrations C).op.IsStableUnderRetracts

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (trivialCofibrations C).HasFactorization (fibrations C)
⊢ (fibrations C).op.HasFactorization (trivialCofibrations C).op

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (cofibrations C).HasFactorization (trivialFibrations C)
⊢ (trivialFibrations C).op.HasFactorization (cofibrations C).op

Tactic:
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 : CofibrantObject C
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (terminal.from X.obj) :=
  (trivialCofibrations C).factorizationData (fibrations C) (terminal.from X.obj)
this : IsCofibrant h.Z
⊢ Fibration h.p

Tactic:
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 : CofibrantObject C
⊢ WeakEquivalence X.iBifibrantResolutionObj.hom

Tactic:
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₁ X₂ : CofibrantObject C
f : X₁ ⟶ X₂
inst✝ : WeakEquivalence f
⊢ WeakEquivalence X₂.iBifibrantResolutionObj

Tactic:
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✝¹ : CategoryWithCofibrations C
inst✝ : (cofibrations C).IsStableUnderRetracts
⊢ ((cofibrations C).inverseImage (Over.forget S)).IsStableUnderRetracts

Tactic:
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✝¹ : CategoryWithFibrations C
inst✝ : (fibrations C).IsStableUnderRetracts
⊢ ((fibrations C).inverseImage (Over.forget S)).IsStableUnderRetracts

Tactic:
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).IsStableUnderRetracts
⊢ ((weakEquivalences C).inverseImage (Over.forget S)).IsStableUnderRetracts

Tactic:
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 C).inverseImage (Over.forget S)).HasTwoOutOfThreeProperty

Tactic:
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 : BifibrantObject C
⊢ WeakEquivalence (mk X.obj).iBifibrantResolutionObj.hom

Tactic:
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✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).HasFactorization (fibrations C)
⊢ (trivialCofibrations C).over.HasFactorization (fibrations C).over

Tactic:
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✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).HasFactorization (trivialFibrations C)
⊢ (cofibrations C).over.HasFactorization (trivialFibrations C).over

Tactic:
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 : BifibrantObject C
this : WeakEquivalence (BifibrantObject.homMk (mk X.obj).iBifibrantResolutionObj.hom)
⊢ IsIso (BifibrantObject.toHoCat.map (BifibrantObject.homMk (mk X.obj).iBifibrantResolutionObj.hom))

Tactic:
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
⊢ IsIso HoCat.adjCounitIso.hom

Tactic:
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 : CofibrantObject C
⊢ WeakEquivalence (HoCat.adjUnit.app (toHoCat.obj X))

Tactic:
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)
⊢ ((weakEquivalences D).inverseImage e.functor).HasTwoOutOfThreeProperty

Tactic:
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 Y : CofibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f
⊢ WeakEquivalence (bifibrantResolutionMap f)

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

Tactic:
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 : HoCat C
⊢ WeakEquivalence (HoCat.adj.unit.app X)

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

Tactic:
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:
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)
A✝ B✝ X✝ Y✝ : C
x✝⁴ : A✝ ⟶ B✝
x✝³ : X✝ ⟶ Y✝
x✝² : Cofibration x✝⁴
x✝¹ : WeakEquivalence x✝⁴
x✝ : Fibration x✝³
⊢ HasLiftingProperty (e.functor.map x✝⁴) (e.functor.map x✝³)

Tactic:
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)
A✝ B✝ X✝ Y✝ : C
x✝⁴ : A✝ ⟶ B✝
x✝³ : X✝ ⟶ Y✝
x✝² : Cofibration x✝⁴
x✝¹ : Fibration x✝³
x✝ : WeakEquivalence x✝³
⊢ HasLiftingProperty (e.functor.map x✝⁴) (e.functor.map x✝³)

Tactic:
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)
⊢ ((trivialCofibrations D).inverseImage e.functor).HasFactorization ((fibrations D).inverseImage e.functor)

Tactic:
infer_instance

Goal state after:
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:
exact Quotient.sound ⟨(Path.Homotopy.reflTransSymm f).symm⟩

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).HasFactorization ((trivialFibrations D).inverseImage e.functor)

Tactic:
infer_instance

Goal state after: