awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
g : Y ⟶ Z
inst_3 : IsFibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} Z
inst_5 : WeakEquivalence g
h : FibrantBrownFactorization g := Classical.arbitrary (FibrantBrownFactorization g)
h₁ :
  ∀ (φ : LeftHomotopyClass X Y),
    ((fun (f : LeftHomotopyClass X (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ↦ f.postcomp h.r) ∘
          fun (f : LeftHomotopyClass X Y) ↦ f.postcomp (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
        φ =
      id φ
⊢ Eq.{v + 1} (α := LeftHomotopyClass X Y → LeftHomotopyClass X Y)
    ((fun (f : LeftHomotopyClass X (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ↦ f.postcomp h.r) ∘
      fun (f : LeftHomotopyClass X Y) ↦ f.postcomp (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
    id

Tactic:
ext φ
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
g : Y ⟶ Z
inst_3 : IsFibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} Z
inst_5 : WeakEquivalence g
h : FibrantBrownFactorization g := Classical.arbitrary (FibrantBrownFactorization g)
φ : LeftHomotopyClass X Y
h₁ :
  ∀ (φ : X ⟶ Y),
    Eq (α := LeftHomotopyClass X Y)
      (((fun (f : LeftHomotopyClass X (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ↦ f.postcomp h.r) ∘
          fun (f : LeftHomotopyClass X Y) ↦ f.postcomp (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
        (mk φ))
      (id (mk φ))
⊢ ((fun (f : LeftHomotopyClass X (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ↦ f.postcomp h.r) ∘
        fun (f : LeftHomotopyClass X Y) ↦ f.postcomp (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
      φ =
    id φ

Tactic:
obtain ⟨φ, rfl⟩ := φ.mk_surjective

Premises used: HomotopicalAlgebra.LeftHomotopyClass.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
g : Y ⟶ Z
inst_3 : IsFibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} Z
inst_5 : WeakEquivalence g
h : FibrantBrownFactorization g := Classical.arbitrary (FibrantBrownFactorization g)
φ : X ⟶ Y
⊢ Eq (α := LeftHomotopyClass X Y)
    (((fun (f : LeftHomotopyClass X (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ↦ f.postcomp h.r) ∘
        fun (f : LeftHomotopyClass X Y) ↦ f.postcomp (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
      (mk φ))
    (id (mk φ))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
g : Y ⟶ Z
inst_3 : IsFibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} Z
inst_5 : WeakEquivalence g
h : FibrantBrownFactorization g := Classical.arbitrary (FibrantBrownFactorization g)
⊢ Function.Bijective (β := LeftHomotopyClass X (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
    fun (f : LeftHomotopyClass X Y) ↦ f.postcomp (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
have hi : Function.Bijective (fun (f : LeftHomotopyClass X Y) ↦ f.postcomp h.i) := by
    rw [← Function.Bijective.of_comp_iff'
      (postcomp_bijective_of_fibration_of_weakEquivalence X h.r)]
    convert! Function.bijective_id
    ext φ
    obtain ⟨φ, rfl⟩ := φ.mk_surjective
    simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
g : Y ⟶ Z
inst_3 : IsFibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} Z
inst_5 : WeakEquivalence g
h : FibrantBrownFactorization g := Classical.arbitrary (FibrantBrownFactorization g)
hi :
  Function.Bijective (β := LeftHomotopyClass X (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
    fun (f : LeftHomotopyClass X Y) ↦ f.postcomp (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ Function.Bijective.{v + 1, v + 1} (α := LeftHomotopyClass X Y) (β := LeftHomotopyClass X Z)
    ((fun (f : LeftHomotopyClass X (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ↦
        f.postcomp (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ∘
      fun (f : LeftHomotopyClass X Y) ↦ f.postcomp (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)))

Tactic:
(postcomp_bijective_of_fibration_of_weakEquivalence X h.p).comp hi

Premises used: CategoryTheory.MorphismProperty.MapFactorizationData.p, HomotopicalAlgebra.LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence, Function.Bijective.comp, HomotopicalAlgebra.FibrantBrownFactorization.toMapFactorizationData
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
g : Y ⟶ Z
inst_3 : IsFibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} Z
inst_5 : WeakEquivalence g
h : FibrantBrownFactorization g := Classical.arbitrary (FibrantBrownFactorization g)
hi :
  Function.Bijective (β := LeftHomotopyClass X (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
    fun (f : LeftHomotopyClass X Y) ↦ f.postcomp (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
h₁ :
  Eq.{v + 1} (α := LeftHomotopyClass X Y → LeftHomotopyClass X Z) (fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g)
    ((fun (f : LeftHomotopyClass X (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ↦
        f.postcomp (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ∘
      fun (f : LeftHomotopyClass X Y) ↦ f.postcomp (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
⊢ Function.Bijective (β := LeftHomotopyClass X Z) fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g

Tactic:
convert! (postcomp_bijective_of_fibration_of_weakEquivalence X h.p).comp hi using 1

Premises used: CategoryTheory.MorphismProperty.MapFactorizationData.p, HomotopicalAlgebra.LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence, Function.Bijective.comp, HomotopicalAlgebra.FibrantBrownFactorization.toMapFactorizationData
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
g : Y ⟶ Z
inst_3 : IsFibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} Z
inst_5 : WeakEquivalence g
h : FibrantBrownFactorization g := Classical.arbitrary (FibrantBrownFactorization g)
hi :
  Function.Bijective (β := LeftHomotopyClass X (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
    fun (f : LeftHomotopyClass X Y) ↦ f.postcomp (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
h₁ :
  ∀ (φ : LeftHomotopyClass X Y),
    φ.postcomp g =
      ((fun (f : LeftHomotopyClass X (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ↦
            f.postcomp (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ∘
          fun (f : LeftHomotopyClass X Y) ↦ f.postcomp (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
        φ
⊢ Eq.{v + 1} (α := LeftHomotopyClass X Y → LeftHomotopyClass X Z) (fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g)
    ((fun (f : LeftHomotopyClass X (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ↦
        f.postcomp (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ∘
      fun (f : LeftHomotopyClass X Y) ↦ f.postcomp (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)))

Tactic:
ext φ
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
g : Y ⟶ Z
inst_3 : IsFibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} Z
inst_5 : WeakEquivalence g
h : FibrantBrownFactorization g := Classical.arbitrary (FibrantBrownFactorization g)
hi :
  Function.Bijective (β := LeftHomotopyClass X (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
    fun (f : LeftHomotopyClass X Y) ↦ f.postcomp (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
φ : LeftHomotopyClass X Y
h₁ :
  ∀ (φ : X ⟶ Y),
    Eq (α := LeftHomotopyClass X Z) (postcomp (mk φ) g)
      (((fun (f : LeftHomotopyClass X (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ↦
            f.postcomp (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ∘
          fun (f : LeftHomotopyClass X Y) ↦ f.postcomp (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
        (mk φ))
⊢ φ.postcomp g =
    ((fun (f : LeftHomotopyClass X (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ↦
          f.postcomp (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ∘
        fun (f : LeftHomotopyClass X Y) ↦ f.postcomp (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
      φ

Tactic:
obtain ⟨φ, rfl⟩ := φ.mk_surjective

Premises used: HomotopicalAlgebra.LeftHomotopyClass.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
g : Y ⟶ Z
inst_3 : IsFibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} Z
inst_5 : WeakEquivalence g
h : FibrantBrownFactorization g := Classical.arbitrary (FibrantBrownFactorization g)
hi :
  Function.Bijective (β := LeftHomotopyClass X (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
    fun (f : LeftHomotopyClass X Y) ↦ f.postcomp (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
φ : X ⟶ Y
⊢ Eq (α := LeftHomotopyClass X Z) (postcomp (mk φ) g)
    (((fun (f : LeftHomotopyClass X (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ↦
          f.postcomp (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))) ∘
        fun (f : LeftHomotopyClass X Y) ↦ f.postcomp (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
      (mk φ))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
left : Function.Injective (β := RightHomotopyClass X Z) fun (g : RightHomotopyClass Y Z) ↦ g.precomp f
right : Function.Surjective (β := RightHomotopyClass X Z) fun (g : RightHomotopyClass Y Z) ↦ g.precomp f
⊢ Function.Bijective (β := RightHomotopyClass X Z) fun (g : RightHomotopyClass Y Z) ↦ g.precomp f

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
f₀ f₁ : RightHomotopyClass Y Z
h :
  Eq.{v + 1} (α := RightHomotopyClass X Z) ((fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) f₀)
    ((fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) f₁)
left :
  ∀ (f₀ : Y ⟶ Z)
    (h :
      Eq.{v + 1} (α := RightHomotopyClass X Z) ((fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) (mk f₀))
        ((fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) f₁)),
    mk f₀ = f₁
⊢ f₀ = f₁

Tactic:
obtain ⟨f₀, rfl⟩ := f₀.mk_surjective

Premises used: HomotopicalAlgebra.RightHomotopyClass.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
f₁ : RightHomotopyClass Y Z
f₀ : Y ⟶ Z
h :
  Eq.{v + 1} (α := RightHomotopyClass X Z) ((fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) (mk f₀))
    ((fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) f₁)
left :
  ∀ (f₁ : Y ⟶ Z)
    (h :
      Eq.{v + 1} (α := RightHomotopyClass X Z) ((fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) (mk f₀))
        ((fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) (mk f₁))),
    Eq (α := RightHomotopyClass Y Z) (mk f₀) (mk f₁)
⊢ mk f₀ = f₁

Tactic:
obtain ⟨f₁, rfl⟩ := f₁.mk_surjective

Premises used: HomotopicalAlgebra.RightHomotopyClass.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
f₀ f₁ : Y ⟶ Z
h :
  Eq.{v + 1} (α := RightHomotopyClass X Z) ((fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) (mk f₀))
    ((fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) (mk f₁))
⊢ RightHomotopyRel (f ≫ f₀) (f ≫ f₁)

Tactic:
simp only [precomp_mk, mk_eq_mk_iff] at h

Premises used: HomotopicalAlgebra.RightHomotopyClass.precomp_mk, HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
f₀ f₁ : Y ⟶ Z
h : RightHomotopyRel (f ≫ f₀) (f ≫ f₁)
left :
  ∀ (P : PathObject.{v, u} Z),
    P.IsGood → ∀ (h : P.RightHomotopy (f ≫ f₀) (f ≫ f₁)), Eq (α := RightHomotopyClass Y Z) (mk f₀) (mk f₁)
⊢ Eq (α := RightHomotopyClass Y Z) (mk f₀) (mk f₁)

Tactic:
obtain ⟨P, _, ⟨h⟩⟩ := h.exists_good_pathObject

Premises used: HomotopicalAlgebra.RightHomotopyRel.exists_good_pathObject
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
f₀ f₁ : Y ⟶ Z
h_1 : RightHomotopyRel (f ≫ f₀) (f ≫ f₁)
P : PathObject.{v, u} Z
left : P.IsGood
h : P.RightHomotopy (f ≫ f₀) (f ≫ f₁)
⊢ CommSq (Z := Limits.prod.{v, u} Z Z) h.h f P.p (prod.lift f₀ f₁)

Tactic:
have sq : CommSq h.h f P.p (prod.lift f₀ f₁) := { }
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
f₀ f₁ : Y ⟶ Z
h_1 : RightHomotopyRel (f ≫ f₀) (f ≫ f₁)
P : PathObject.{v, u} Z
left_1 : P.IsGood
h : P.RightHomotopy (f ≫ f₀) (f ≫ f₁)
sq : CommSq (Z := Limits.prod.{v, u} Z Z) h.h f P.p (prod.lift f₀ f₁)
left : RightHomotopyRel f₀ f₁
⊢ Eq (α := RightHomotopyClass Y Z) (mk f₀) (mk f₁)

Tactic:
rw [mk_eq_mk_iff]

Premises used: HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
f₀ f₁ : Y ⟶ Z
h_1 : RightHomotopyRel (f ≫ f₀) (f ≫ f₁)
P : PathObject.{v, u} Z
left : P.IsGood
h : P.RightHomotopy (f ≫ f₀) (f ≫ f₁)
sq : CommSq (Z := Limits.prod.{v, u} Z Z) h.h f P.p (prod.lift f₀ f₁)
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (sq.lift ≫ P.p) prod.fst =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift f₀ f₁) prod.fst

Tactic:
have := sq.fac_right =≫ prod.fst
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
f₀ f₁ : Y ⟶ Z
h_1 : RightHomotopyRel (f ≫ f₀) (f ≫ f₁)
P : PathObject.{v, u} Z
left : P.IsGood
h : P.RightHomotopy (f ≫ f₀) (f ≫ f₁)
sq : CommSq (Z := Limits.prod.{v, u} Z Z) h.h f P.p (prod.lift f₀ f₁)
this :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (sq.lift ≫ P.p) prod.fst =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift f₀ f₁) prod.fst
rwa :
  ∀
    (this :
      sq.lift ≫ CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) P.p prod.fst =
        CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift f₀ f₁) prod.fst),
    sq.lift ≫ P.p₀ = f₀
rwa₁ :
  ∀ (this : sq.lift ≫ P.p₀ = CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift f₀ f₁) prod.fst),
    sq.lift ≫ P.p₀ = f₀
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : sq.lift ≫ P.p₀ = f₀), sq.lift ≫ P.p₀ = f₀
⊢ sq.lift ≫ P.p₀ = f₀

Tactic:
rwa [Category.assoc, P.p_fst, prod.lift_fst] at this

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.prod.lift_fst, HomotopicalAlgebra.PrepathObject.p_fst, HomotopicalAlgebra.PathObject.toPrepathObject
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
f₀ f₁ : Y ⟶ Z
h_1 : RightHomotopyRel (f ≫ f₀) (f ≫ f₁)
P : PathObject.{v, u} Z
left : P.IsGood
h : P.RightHomotopy (f ≫ f₀) (f ≫ f₁)
sq : CommSq (Z := Limits.prod.{v, u} Z Z) h.h f P.p (prod.lift f₀ f₁)
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (sq.lift ≫ P.p) prod.snd =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift f₀ f₁) prod.snd

Tactic:
have := sq.fac_right =≫ prod.snd
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
f₀ f₁ : Y ⟶ Z
h_1 : RightHomotopyRel (f ≫ f₀) (f ≫ f₁)
P : PathObject.{v, u} Z
left : P.IsGood
h : P.RightHomotopy (f ≫ f₀) (f ≫ f₁)
sq : CommSq (Z := Limits.prod.{v, u} Z Z) h.h f P.p (prod.lift f₀ f₁)
this :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (sq.lift ≫ P.p) prod.snd =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift f₀ f₁) prod.snd
rwa :
  ∀
    (this :
      sq.lift ≫ CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) P.p prod.snd =
        CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift f₀ f₁) prod.snd),
    sq.lift ≫ P.p₁ = f₁
rwa₁ :
  ∀ (this : sq.lift ≫ P.p₁ = CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift f₀ f₁) prod.snd),
    sq.lift ≫ P.p₁ = f₁
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : sq.lift ≫ P.p₁ = f₁), sq.lift ≫ P.p₁ = f₁
⊢ sq.lift ≫ P.p₁ = f₁

Tactic:
rwa [Category.assoc, P.p_snd, prod.lift_snd] at this

Premises used: HomotopicalAlgebra.PrepathObject.p_snd, CategoryTheory.Category.assoc, HomotopicalAlgebra.PathObject.toPrepathObject, CategoryTheory.Limits.prod.lift_snd
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
f₀ f₁ : Y ⟶ Z
h_1 : RightHomotopyRel (f ≫ f₀) (f ≫ f₁)
P : PathObject.{v, u} Z
left : P.IsGood
h : P.RightHomotopy (f ≫ f₀) (f ≫ f₁)
sq : CommSq (Z := Limits.prod.{v, u} Z Z) h.h f P.p (prod.lift f₀ f₁)
⊢ RightHomotopyRel f₀ f₁

Tactic:
exact ⟨P,
      ⟨{h := sq.lift
        h₀ := by
          have := sq.fac_right =≫ prod.fst
          rwa [Category.assoc, P.p_fst, prod.lift_fst] at this
        h₁ := by
          have := sq.fac_right =≫ prod.snd
          rwa [Category.assoc, P.p_snd, prod.lift_snd] at this }⟩⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
φ : RightHomotopyClass X Z
right :
  ∀ (φ : X ⟶ Z),
    ∃ (a : RightHomotopyClass Y Z),
      Eq (α := RightHomotopyClass X Z) ((fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) a) (mk φ)
⊢ ∃ (a : RightHomotopyClass Y Z), (fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) a = φ

Tactic:
obtain ⟨φ, rfl⟩ := φ.mk_surjective

Premises used: HomotopicalAlgebra.RightHomotopyClass.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
φ : X ⟶ Z
⊢ CommSq (Z := terminal.{v, u} C) φ f (terminal.from Z) (terminal.from Y)

Tactic:
have sq : CommSq φ f (terminal.from _) (terminal.from _) := { }
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
φ : X ⟶ Z
sq : CommSq (Z := terminal.{v, u} C) φ f (terminal.from Z) (terminal.from Y)
⊢ Eq (α := RightHomotopyClass X Z) ((fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) (mk sq.lift)) (mk φ)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
φ : X ⟶ Z
sq : CommSq (Z := terminal.{v, u} C) φ f (terminal.from Z) (terminal.from Y)
⊢ ∃ (a : RightHomotopyClass Y Z),
    Eq (α := RightHomotopyClass X Z) ((fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) a) (mk φ)

Tactic:
exact ⟨mk sq.lift, by simp⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : IsCofibrant.{v, u} X
inst_4 : IsCofibrant.{v, u} Y
inst_5 : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
rw :
  Function.Bijective.{v + 1, v + 1} (α := RightHomotopyClass Y Z) (β := RightHomotopyClass Y Z)
    ((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦ g.precomp h.s) ∘
      fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))
⊢ Function.Bijective (β := RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z)
    fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
rw [← Function.Bijective.of_comp_iff'
      (precomp_bijective_of_cofibration_of_weakEquivalence Z h.s)]

Premises used: HomotopicalAlgebra.CofibrantBrownFactorization.s, HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence, Function.Bijective.of_comp_iff'
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : IsCofibrant.{v, u} X
inst_4 : IsCofibrant.{v, u} Y
inst_5 : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
⊢ Function.Bijective.{v + 1, v + 1} (α := RightHomotopyClass Y Z) id

Tactic:
Function.bijective_id

Premises used: Function.bijective_id
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : IsCofibrant.{v, u} X
inst_4 : IsCofibrant.{v, u} Y
inst_5 : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
h₁ :
  Eq.{v + 1} (α := RightHomotopyClass Y Z → RightHomotopyClass Y Z)
    ((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦ g.precomp h.s) ∘
      fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))
    id
⊢ Function.Bijective.{v + 1, v + 1} (α := RightHomotopyClass Y Z) (β := RightHomotopyClass Y Z)
    ((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦ g.precomp h.s) ∘
      fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))

Tactic:
convert! Function.bijective_id

Premises used: Function.bijective_id