mathlib-initiative/mathlib-tactics huggingface dataset:
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
this : L.map (homMk P.p₀) = L.map (homMk P.p₁)
⊢ L.map f = L.map g

Tactic:
by

Goal state after:
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
p : Path x₀ x₁
x : ↑I
⊢ p ⟨reflTransSymmAux (1, x), ⋯⟩ = (p.trans p.symm).toContinuousMap x

Tactic:
by

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₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w✝ : W s
f : T ⟶ Y
this : IsIso (G.map s)
⊢ f ≫
      { Y' := F.obj (G.obj Y), f := adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f), s := adj.unit.app Y,
          hs := ⋯ }.s =
    s ≫
      { Y' := F.obj (G.obj Y), f := adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f), s := adj.unit.app Y,
          hs := ⋯ }.f

Tactic:
by

Goal state after:
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
p : Path x₀ x₁
t : ↑I
⊢ ∀ x ∈ {0, 1},
    { toFun := fun x ↦ p ⟨reflTransSymmAux (t, x), ⋯⟩, continuous_toFun := ⋯ } x = (Path.refl x₀).toContinuousMap x

Tactic:
by

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₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y : C₁
φ : W.RightFraction X Y
⊢ ∃ ψ, φ.f ≫ ψ.s = φ.s ≫ ψ.f

Tactic:
by

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₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
x✝ : W s
h : s ≫ f₁ = s ≫ f₂
⊢ W s

Tactic:
by

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

Goal state before:
pp: ⊢ Continuous Subtype.val

Tactic:
by

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

Goal state before:
pp: ⊢ ContinuousOn (fun x ↦ 2 * ↑x) {x | ↑x ≤ 1 / 2}

Tactic:
by

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
⊢ weakEquivalences (CofibrantObject C) (homMk P.ι)

Tactic:
by

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

Goal state before:
pp: ⊢ ContinuousOn (fun x ↦ 1) {x | 1 / 2 ≤ ↑x}

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (x : ↑I), ↑x = 1 / 2 → 2 * ↑x = 1

Tactic:
by

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
⊢ (homRel C).FactorsThroughLocalization (weakEquivalences (CofibrantObject C))

Tactic:
by

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₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
x✝ : W s
h : s ≫ f₁ = s ≫ f₂
⊢ ∃ Y' t, ∃ (_ : W t), f₁ ≫ t = f₂ ≫ t

Tactic:
by

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
⊢ (toHoCatLocalizerMorphism C).IsLocalizedEquivalence

Tactic:
by

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₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (π.map (TopCat.ofHom f)).map p ≫ ⟦H.evalAt x₁⟧ = H.diagonalPath' p ∧
    ⟦H.evalAt x₀⟧ ≫ (π.map (TopCat.ofHom g)).map p = H.diagonalPath' p

Tactic:
by

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

Goal state before:
pp: t : ↑I
⊢ transReflReparamAux t ∈ I

Tactic:
by

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

Goal state before:
pp: ⊢ transReflReparamAux 0 = 0

Tactic:
by

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

Goal state before:
pp: ⊢ transReflReparamAux 1 = 1

Tactic:
by

Goal state after:
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
p : Path x₀ x₁
⊢ Continuous fun t ↦ ⟨transReflReparamAux t, ⋯⟩

Tactic:
by

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
W : MorphismProperty C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
Φ : W.Localization ⥤ C₂ := Localization.lift G hW W.Q
⊢ W.Q ⋙ Φ ≅ G

Tactic:
by

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
⊢ ∃ X', ∃ (_ : IsCofibrant X'), ∃ p, Fibration p ∧ WeakEquivalence p

Tactic:
by

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 : C
f : X ⟶ Y
⊢ initial.to (resolutionObj Y) ≫ pResolutionObj Y = initial.to (resolutionObj X) ≫ pResolutionObj X ≫ f

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
⊢ p.trans (Path.refl x₁) = p.reparam (fun t ↦ ⟨transReflReparamAux t, ⋯⟩) trans_refl_reparam._proof_1 ⋯ ⋯

Tactic:
by

Goal state after:
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
p : Path x₀ x₁
⊢ (p.symm.trans (Path.refl x₀)).symm = (Path.refl x₀).trans p

Tactic:
by

Goal state after:
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
p : Path x₀ x₁
⊢ p.symm.symm = p

Tactic:
by

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

Goal state before:
pp: ⊢ Continuous fun x ↦ 1 / 4

Tactic:
by

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 : C
f : X ⟶ Y
⊢ ∃ g, g ≫ pResolutionObj Y = pResolutionObj X ≫ f

Tactic:
by

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

Goal state before:
pp: ⊢ ContinuousOn (fun x ↦ 2 * ↑x) {x | ↑x ≤ 1 / 4}

Tactic:
by

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

Goal state before:
pp: ⊢ ContinuousOn (fun x ↦ ↑x + 1 / 4) {x | ↑x ≤ 1 / 2}

Tactic:
by

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

Goal state before:
pp: ⊢ ContinuousOn (fun x ↦ 1 / 2 * (↑x + 1)) {x | 1 / 2 ≤ ↑x}

Tactic:
by

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
W : MorphismProperty C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
Φ : W.Localization ⥤ C₂ := Localization.lift G hW W.Q
e : W.Q ⋙ Φ ≅ G := Localization.fac G hW W.Q
⊢ IsIso (Functor.whiskerRight adj.unit W.Q)

Tactic:
by

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 : C
f : X ⟶ Y
⊢ WeakEquivalence (resolutionMap f) ↔ WeakEquivalence f

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (x : ↑I), ↑x = 1 / 2 → ↑x + 1 / 4 = 1 / 2 * (↑x + 1)

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (x : ↑I), ↑x = 1 / 4 → 2 * ↑x = if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)

Tactic:
by

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
W : MorphismProperty C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
⊢ G.IsLocalization W

Tactic:
by

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
W : MorphismProperty C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.counit
⊢ G.IsLocalization W

Tactic:
by

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

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
inst✝ : IsCofibrant X
Y : C
f g : X ⟶ resolutionObj Y
h : LeftHomotopyRel (f ≫ pResolutionObj Y) (g ≫ pResolutionObj Y)
⊢ toHoCat.map (homMk f) = toHoCat.map (homMk g)

Tactic:
by

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

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
⊢ LeftHomotopyRel (resolutionMap (𝟙 X) ≫ pResolutionObj X) (𝟙 (mk (resolutionObj X)).obj ≫ pResolutionObj X)

Tactic:
by

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
⊢ toHoCat.map (homMk (resolutionMap (𝟙 X))) = 𝟙 (toHoCat.obj (mk (resolutionObj X)))

Tactic:
by

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

Goal state before:
pp: t : ↑I
⊢ transAssocReparamAux t ∈ I

Tactic:
by

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₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ LeftHomotopyRel (resolutionMap (f ≫ g) ≫ pResolutionObj X₃)
    (((homMk (resolutionMap f)).hom ≫ (homMk (resolutionMap g)).hom) ≫ pResolutionObj X₃)

Tactic:
by

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

Goal state before:
pp: ⊢ transAssocReparamAux 0 = 0

Tactic:
by

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₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ toHoCat.map (homMk (resolutionMap (f ≫ g))) =
    toHoCat.map (homMk (resolutionMap f)) ≫ toHoCat.map (homMk (resolutionMap g))

Tactic:
by

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

Goal state before:
pp: ⊢ transAssocReparamAux 1 = 1

Tactic:
by

Goal state after:
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₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
⊢ Continuous fun t ↦ ⟨transAssocReparamAux t, ⋯⟩

Tactic:
by

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✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
h : weakEquivalences C x✝
⊢ (weakEquivalences (HoCat C)).inverseImage resolution x✝

Tactic:
by

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✝¹ x✝ : CofibrantObject C
f : x✝¹ ⟶ x✝
⊢ homMk (resolutionMap (ι.map f)) ≫ { hom := pResolutionObj (ι.obj x✝) } = { hom := pResolutionObj (ι.obj x✝¹) } ≫ f

Tactic:
by

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 (HoCat.ιCompResolutionNatTrans.app X)

Tactic:
by

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))
⊢ IsIso (Functor.whiskerRight HoCat.ιCompResolutionNatTrans L)

Tactic:
by

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✝¹ x✝ : C
f : x✝¹ ⟶ x✝
⊢ (resolution ⋙ toLocalization L).map f ≫ L.map (pResolutionObj x✝) = L.map (pResolutionObj x✝¹) ≫ L.map f

Tactic:
by

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)
⊢ IsIso (HoCat.resolutionCompToLocalizationNatTrans L)

Tactic:
by

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
⊢ weakEquivalences (CofibrantObject C) ≤ (weakEquivalences C).inverseImage ι

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
R : (localizerMorphism C).LeftResolution X
⊢ WeakEquivalence R.w

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
⊢ weakEquivalences C (HoCat.pResolutionObj X)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
R₀ : (localizerMorphism C).LeftResolution X :=
  { X₁ := mk (HoCat.resolutionObj X), w := HoCat.pResolutionObj X, hw := ⋯ }
R : (localizerMorphism C).LeftResolution X
⊢ initial.to ((localizerMorphism C).functor.obj R₀.X₁) ≫ R₀.w =
    initial.to ((localizerMorphism C).functor.obj R.X₁) ≫ R.w

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
R₀ : (localizerMorphism C).LeftResolution X :=
  { X₁ := mk (HoCat.resolutionObj X), w := HoCat.pResolutionObj X, hw := ⋯ }
R : (localizerMorphism C).LeftResolution X
⊢ Nonempty (Zigzag R R₀)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
⊢ IsConnected ((localizerMorphism C).LeftResolution X)

Tactic:
by

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
⊢ (localizerMorphism C).IsLocalizedEquivalence

Tactic:
by

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 ((localizerMorphism C).functor.obj X)

Tactic:
by

Goal state after:
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
⊢ leftHomotopyClassToHom L = rightHomotopyClassToHom L ∘ ⇑leftHomotopyClassEquivRightHomotopyClass

Tactic:
by

Goal state after:
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
⊢ Function.Bijective (leftHomotopyClassToHom L) ↔ Function.Bijective (rightHomotopyClassToHom L)

Tactic:
by

Goal state after:
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
this : ∀ (Y : C) [IsFibrant Y], IsCofibrant Y → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsCofibrant Y
Y' : C
w✝ : IsCofibrant Y'
p : Y' ⟶ Y
left✝ : Fibration p
right✝ : WeakEquivalence p
x✝ : IsFibrant Y'
hY' : Function.Bijective (leftHomotopyClassToHom L)
⊢ weakEquivalences C p

Tactic:
rwa [← weakEquivalence_iff]

Goal state after:
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
this : ∀ (Y : C) [IsFibrant Y], IsCofibrant Y → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsCofibrant Y
Y' : C
w✝ : IsCofibrant Y'
p : Y' ⟶ Y
left✝ : Fibration p
right✝ : WeakEquivalence p
x✝ : IsFibrant Y'
hY' : Function.Bijective (leftHomotopyClassToHom L)
⊢ weakEquivalences C p

Tactic:
by

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 : BifibrantObject C
f g : X ⟶ Y
⊢ homRel C f g ↔ LeftHomotopyRel f.hom g.hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
⊢ toHoCat.Full

Tactic:
by

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} (HoCat C)

Tactic:
by

Goal state after:
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
Y : C
inst✝ : IsFibrant Y
h✝¹ : IsCofibrant Y
this : ∀ (X : C) [IsCofibrant X], IsFibrant X → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsFibrant X
X' : C
i : X ⟶ X'
left✝¹ : Cofibration i
left✝ : WeakEquivalence i
right✝ : IsFibrant X'
x✝ : IsCofibrant X'
hX' : Function.Bijective (rightHomotopyClassToHom L)
⊢ weakEquivalences C i

Tactic:
rwa [← weakEquivalence_iff]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
H : (weakEquivalences (BifibrantObject C)).IsInvertedBy F
K L : BifibrantObject C
f g : K ⟶ L
h✝ : homRel C f g
P : PathObject L.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this : IsCofibrant P.P
⊢ weakEquivalences (BifibrantObject C) (homMk P.ι)

Tactic:
by

Goal state after:
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
Y : C
inst✝ : IsFibrant Y
h✝¹ : IsCofibrant Y
this : ∀ (X : C) [IsCofibrant X], IsFibrant X → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsFibrant X
X' : C
i : X ⟶ X'
left✝¹ : Cofibration i
left✝ : WeakEquivalence i
right✝ : IsFibrant X'
x✝ : IsCofibrant X'
hX' : Function.Bijective (rightHomotopyClassToHom L)
⊢ weakEquivalences C i

Tactic:
by

Goal state after:
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✝ Y : C
inst✝¹ : IsFibrant Y
h✝¹ : IsCofibrant Y
X : C
inst✝ : IsCofibrant X
h✝ : IsFibrant X
E : BifibrantObject.HoCat C ≌ H :=
  Localization.uniq BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L) (weakEquivalences (BifibrantObject C))
e : BifibrantObject.toHoCat ⋙ E.functor ≅ BifibrantObject.ι ⋙ L :=
  Localization.compUniqFunctor BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L) (weakEquivalences (BifibrantObject C))
⊢ rightHomotopyClassToHom L =
    ⇑(BifibrantObject.HoCat.homEquivRight.trans
        (E.fullyFaithfulFunctor.homEquiv.trans
          ((e.app (BifibrantObject.mk X)).homCongr (e.app (BifibrantObject.mk Y)))))

Tactic:
by

Goal state after:
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
⊢ Function.Bijective (rightHomotopyClassToHom L)

Tactic:
by

Goal state after: