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).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
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
⊢ IsIso (HoCat.bifibrantResolution.map (toHoCat.map f))

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f
⊢ IsIso (HoCat.bifibrantResolution.map (toHoCat.map f))
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
⊢ IsIso (BifibrantObject.toHoCat.map (bifibrantResolutionMap f))

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f
⊢ IsIso (BifibrantObject.toHoCat.map (bifibrantResolutionMap 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)
⊢ ((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.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:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f
⊢ WeakEquivalence (bifibrantResolutionMap f)
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:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : HoCat C
⊢ WeakEquivalence (HoCat.adj.unit.app 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)
⊢ ((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)
⊢ ((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.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:
]

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)
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✝³)
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:
]

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)
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✝³)
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
⊢ ∀ {W X_1 Y Z : FundamentalGroupoid X} (f : Path.Homotopic.Quotient W.as X_1.as)
    (g : Path.Homotopic.Quotient X_1.as Y.as) (h : Path.Homotopic.Quotient Y.as Z.as),
    (f.trans g).trans h = f.trans (g.trans h)

Tactic:
rintro _ _ _ _ ⟨f⟩ ⟨g⟩ ⟨h⟩

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.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.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.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
j : J.R
⊢ F.map (c.ι (J.snd j) ≫ d.snd j) = F.map (c.ι (J.snd j) ≫ d.snd j)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
U✝ V✝ : C
φ : U✝ ⟶ V✝
x : F₁.obj U✝
hx : x ∈ A.obj U✝
h : (ConcreteCategory.hom (f.app U✝)) ⟨x, hx⟩ = (ConcreteCategory.hom (g.app U✝)) ⟨x, hx⟩
⊢ (ConcreteCategory.hom (F₂.map φ)) ((ConcreteCategory.hom (g.app U✝)) ⟨x, hx⟩) =
    (ConcreteCategory.hom (F₂.map φ)) ((ConcreteCategory.hom (g.app U✝)) ⟨x, hx⟩)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
G : C ⥤ Type w
φ : G ⟶ A.toFunctor
⊢ range (φ ≫ A.ι) ≤ Subfunctor.equalizer f g ↔ (φ ≫ f).app = (φ ≫ g).app

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
G : C ⥤ Type w
φ : G ⟶ A.toFunctor
⊢ range (φ ≫ A.ι) ≤ Subfunctor.equalizer f g ↔ (φ ≫ f).app = (φ ≫ g).app
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 : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
j : J.L
⊢ F.map (d.snd j ≫ c.π (J.snd j)) = F.map (d.snd j ≫ c.π (J.snd j))

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
⊢ Subfunctor.equalizer f g = A ↔ A ≤ Subfunctor.equalizer f g

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
⊢ Subfunctor.equalizer f g = A ↔ A ≤ Subfunctor.equalizer f g
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
h : Subfunctor.equalizer f g = A
⊢ A ≤ A

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
⊢ (I.fst default ≫ if hk : J.fst default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) =
    I.snd default ≫ if hk : J.snd default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
⊢ (I.fst default ≫ if hk : J.fst default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) =
    I.snd default ≫ if hk : J.snd default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
⊢ s.inl = s.inl

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
⊢ s.inr = s.inr

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
⊢ (if hk : J.snd default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) = s.inr

Tactic:
rw [dif_neg h'.symm, eqToHom_refl, Category.id_comp]

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
inst✝ : CompleteLattice T
x₁ x₂ x₃ x₄ : T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ (⨆ i, bif i then x₃ else x₂) = ⨆ b, bif b then x₃ else x₂

Tactic:
]

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
inst✝ : CompleteLattice T
x₁ x₂ x₃ x₄ : T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ (⨆ i, bif i then x₃ else x₂) = x₄

Tactic:
rw [← sq.sup_eq, sup_comm, sup_eq_iSup]

Goal state after: