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
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : LeftHomotopyRel f g
Q : PathObject.{v, u} Y
inst_3 : Q.IsGood
P : Cylinder.{v, u} X := ⋯.choose (p := fun (P : Cylinder.{v, u} X) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g))
h : ⋯.choose (p := fun (P : Cylinder.{v, u} X) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)).LeftHomotopy f g
h' : ⋯.choose (p := fun (P' : Cylinder.{v, u} X) ↦ P'.IsGood ∧ Nonempty.{v + 1} (P'.LeftHomotopy f g)).IsGood
sq : CommSq (Z := Limits.prod.{v, u} Y Y) (f ≫ Q.ι) P.i₀ Q.p (prod.lift (P.π ≫ f) h.h)
this :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (sq.lift ≫ Q.p) prod.snd =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (P.π ≫ f) h.h) prod.snd
⊢ sq.lift ≫ Q.p₁ = h.h

Tactic:
rw [Category.assoc, Q.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
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : LeftHomotopyRel f g
Q : PathObject.{v, u} Y
inst_3 : Q.IsGood
P : Cylinder.{v, u} X := ⋯.choose (p := fun (P : Cylinder.{v, u} X) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g))
h : ⋯.choose (p := fun (P : Cylinder.{v, u} X) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)).LeftHomotopy f g
h' : ⋯.choose (p := fun (P' : Cylinder.{v, u} X) ↦ P'.IsGood ∧ Nonempty.{v + 1} (P'.LeftHomotopy f g)).IsGood
sq : CommSq (Z := Limits.prod.{v, u} Y Y) (f ≫ Q.ι) P.i₀ Q.p (prod.lift (P.π ≫ f) h.h)
this : sq.lift ≫ Q.p₁ = h.h
⊢ (P.i₁ ≫ sq.lift) ≫ Q.p₁ = g

Tactic:
simp [this]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h : LeftHomotopyRel f g
obtain : ∀ (P : PathObject.{v, u} Y), P.IsVeryGood → RightHomotopyRel f g
⊢ RightHomotopyRel f g

Tactic:
obtain ⟨P, _⟩ := PathObject.exists_very_good Y

Premises used: HomotopicalAlgebra.PathObject.exists_very_good
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h : LeftHomotopyRel f g
P : PathObject.{v, u} Y
h_1 : P.IsVeryGood
⊢ RightHomotopyRel f g

Tactic:
⟨_, ⟨h.rightHomotopy P⟩⟩

Premises used: HomotopicalAlgebra.LeftHomotopyRel.rightHomotopy, Nonempty.intro, Exists.intro, HomotopicalAlgebra.RightHomotopyRel
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h : LeftHomotopyRel f g
P : PathObject.{v, u} Y
h_1 : P.IsVeryGood
⊢ RightHomotopyRel f g

Tactic:
exact ⟨_, ⟨h.rightHomotopy P⟩⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h_1 : RightHomotopyRel f g
Q : Cylinder.{v, u} X
inst_3 : Q.IsGood
P : PathObject.{v, u} Y :=
  ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g))
h : ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)).RightHomotopy f g
h' : ⋯.choose (p := fun (P' : PathObject.{v, u} Y) ↦ P'.IsGood ∧ Nonempty.{v + 1} (P'.RightHomotopy f g)).IsGood
sq : CommSq (W := coprod.{v, u} X X) (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f)
⊢ CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (Q.i ≫ sq.lift) =
    CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (coprod.desc (f ≫ P.ι) h.h)

Tactic:
have := coprod.inl ≫= sq.fac_left
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h_1 : RightHomotopyRel f g
Q : Cylinder.{v, u} X
inst_3 : Q.IsGood
P : PathObject.{v, u} Y :=
  ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g))
h : ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)).RightHomotopy f g
h' : ⋯.choose (p := fun (P' : PathObject.{v, u} Y) ↦ P'.IsGood ∧ Nonempty.{v + 1} (P'.RightHomotopy f g)).IsGood
sq : CommSq (W := coprod.{v, u} X X) (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f)
this :
  CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (Q.i ≫ sq.lift) =
    CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (coprod.desc (f ≫ P.ι) h.h)
⊢ Q.i₀ ≫ sq.lift = f ≫ P.ι

Tactic:
rw [Q.inl_i_assoc, coprod.inl_desc] at this

Premises used: HomotopicalAlgebra.Cylinder.toPrecylinder, CategoryTheory.Limits.coprod.inl_desc, HomotopicalAlgebra.Precylinder.inl_i_assoc
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h_1 : RightHomotopyRel f g
Q : Cylinder.{v, u} X
inst_3 : Q.IsGood
P : PathObject.{v, u} Y :=
  ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g))
h : ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)).RightHomotopy f g
h' : ⋯.choose (p := fun (P' : PathObject.{v, u} Y) ↦ P'.IsGood ∧ Nonempty.{v + 1} (P'.RightHomotopy f g)).IsGood
sq : CommSq (W := coprod.{v, u} X X) (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f)
this : Q.i₀ ≫ sq.lift = f ≫ P.ι
⊢ Q.i₀ ≫ sq.lift ≫ P.p₁ = f

Tactic:
simp [reassoc_of% 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
f g : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h_1 : RightHomotopyRel f g
Q : Cylinder.{v, u} X
inst_3 : Q.IsGood
P : PathObject.{v, u} Y :=
  ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g))
h : ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)).RightHomotopy f g
h' : ⋯.choose (p := fun (P' : PathObject.{v, u} Y) ↦ P'.IsGood ∧ Nonempty.{v + 1} (P'.RightHomotopy f g)).IsGood
sq : CommSq (W := coprod.{v, u} X X) (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f)
⊢ CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (Q.i ≫ sq.lift) =
    CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (coprod.desc (f ≫ P.ι) h.h)

Tactic:
have := coprod.inr ≫= sq.fac_left
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h_1 : RightHomotopyRel f g
Q : Cylinder.{v, u} X
inst_3 : Q.IsGood
P : PathObject.{v, u} Y :=
  ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g))
h : ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)).RightHomotopy f g
h' : ⋯.choose (p := fun (P' : PathObject.{v, u} Y) ↦ P'.IsGood ∧ Nonempty.{v + 1} (P'.RightHomotopy f g)).IsGood
sq : CommSq (W := coprod.{v, u} X X) (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f)
this :
  CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (Q.i ≫ sq.lift) =
    CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (coprod.desc (f ≫ P.ι) h.h)
⊢ Q.i₁ ≫ sq.lift = h.h

Tactic:
rw [Q.inr_i_assoc, coprod.inr_desc] at this

Premises used: HomotopicalAlgebra.Precylinder.inr_i_assoc, HomotopicalAlgebra.Cylinder.toPrecylinder, CategoryTheory.Limits.coprod.inr_desc
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h_1 : RightHomotopyRel f g
Q : Cylinder.{v, u} X
inst_3 : Q.IsGood
P : PathObject.{v, u} Y :=
  ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g))
h : ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)).RightHomotopy f g
h' : ⋯.choose (p := fun (P' : PathObject.{v, u} Y) ↦ P'.IsGood ∧ Nonempty.{v + 1} (P'.RightHomotopy f g)).IsGood
sq : CommSq (W := coprod.{v, u} X X) (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f)
this : Q.i₁ ≫ sq.lift = h.h
⊢ Q.i₁ ≫ sq.lift ≫ P.p₁ = g

Tactic:
simp [reassoc_of% this, P]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
f g : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h : RightHomotopyRel f g
obtain : ∀ (P : Cylinder.{v, u} X), P.IsVeryGood → LeftHomotopyRel f g
⊢ LeftHomotopyRel f g

Tactic:
obtain ⟨P, _⟩ := Cylinder.exists_very_good X

Premises used: HomotopicalAlgebra.Cylinder.exists_very_good
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
f g : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h : RightHomotopyRel f g
P : Cylinder.{v, u} X
h_1 : P.IsVeryGood
⊢ LeftHomotopyRel f g

Tactic:
⟨P, ⟨h.leftHomotopy P⟩⟩

Premises used: HomotopicalAlgebra.LeftHomotopyRel, Nonempty.intro, Exists.intro, HomotopicalAlgebra.RightHomotopyRel.leftHomotopy
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
f g : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h : RightHomotopyRel f g
P : Cylinder.{v, u} X
h_1 : P.IsVeryGood
⊢ LeftHomotopyRel f g

Tactic:
exact ⟨P, ⟨h.leftHomotopy P⟩⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsFibrant.{v, u} Y
⊢ LeftHomotopyRel f g ↔ RightHomotopyRel f g

Tactic:
⟨fun h ↦ h.rightHomotopyRel, fun h ↦ h.leftHomotopyRel⟩

Premises used: Iff.intro, HomotopicalAlgebra.RightHomotopyRel.leftHomotopyRel, HomotopicalAlgebra.LeftHomotopyRel.rightHomotopyRel
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsFibrant.{v, u} Y
h : LeftHomotopyRel f g
Q : Cylinder.{v, u} X
inst_4 : Q.IsGood
rwa rwa₁ rwa₂ rwa₃ : LeftHomotopyRel f g
⊢ RightHomotopyRel f g

Tactic:
rwa [← leftHomotopyRel_iff_rightHomotopyRel]

Premises used: HomotopicalAlgebra.leftHomotopyRel_iff_rightHomotopyRel
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsFibrant.{v, u} Y
h : RightHomotopyRel f g
P : PathObject.{v, u} Y
inst_4 : P.IsGood
rwa rwa₁ rwa₂ rwa₃ : RightHomotopyRel f g
⊢ LeftHomotopyRel f g

Tactic:
rwa [leftHomotopyRel_iff_rightHomotopyRel]

Premises used: HomotopicalAlgebra.leftHomotopyRel_iff_rightHomotopyRel
-- 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 : Fibration g
inst_4 : WeakEquivalence g
left : Function.Injective (β := LeftHomotopyClass X Z) fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g
right : Function.Surjective (β := LeftHomotopyClass X Z) fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g
⊢ Function.Bijective (β := LeftHomotopyClass X Z) fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g

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 : IsCofibrant.{v, u} X
g : Y ⟶ Z
inst_3 : Fibration g
inst_4 : WeakEquivalence g
f₀ f₁ : LeftHomotopyClass X Y
h :
  Eq.{v + 1} (α := LeftHomotopyClass X Z) ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) f₀)
    ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) f₁)
left :
  ∀ (f₀ : X ⟶ Y)
    (h :
      Eq.{v + 1} (α := LeftHomotopyClass X Z) ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) (mk f₀))
        ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) f₁)),
    mk f₀ = f₁
⊢ f₀ = f₁

Tactic:
obtain ⟨f₀, rfl⟩ := f₀.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 : Fibration g
inst_4 : WeakEquivalence g
f₁ : LeftHomotopyClass X Y
f₀ : X ⟶ Y
h :
  Eq.{v + 1} (α := LeftHomotopyClass X Z) ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) (mk f₀))
    ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) f₁)
left :
  ∀ (f₁ : X ⟶ Y)
    (h :
      Eq.{v + 1} (α := LeftHomotopyClass X Z) ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) (mk f₀))
        ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) (mk f₁))),
    Eq (α := LeftHomotopyClass X Y) (mk f₀) (mk f₁)
⊢ mk f₀ = f₁

Tactic:
obtain ⟨f₁, rfl⟩ := f₁.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 : Fibration g
inst_4 : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h :
  Eq.{v + 1} (α := LeftHomotopyClass X Z) ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) (mk f₀))
    ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) (mk f₁))
⊢ LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)

Tactic:
simp only [postcomp_mk, mk_eq_mk_iff] at h

Premises used: HomotopicalAlgebra.LeftHomotopyClass.mk_eq_mk_iff, HomotopicalAlgebra.LeftHomotopyClass.postcomp_mk
-- 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 : Fibration g
inst_4 : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h : LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)
left :
  ∀ (P : Cylinder.{v, u} X),
    P.IsGood → ∀ (h : P.LeftHomotopy (f₀ ≫ g) (f₁ ≫ g)), Eq (α := LeftHomotopyClass X Y) (mk f₀) (mk f₁)
⊢ Eq (α := LeftHomotopyClass X Y) (mk f₀) (mk f₁)

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

Premises used: HomotopicalAlgebra.LeftHomotopyRel.exists_good_cylinder
-- 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 : Fibration g
inst_4 : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h_1 : LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)
P : Cylinder.{v, u} X
left : P.IsGood
h : P.LeftHomotopy (f₀ ≫ g) (f₁ ≫ g)
⊢ CommSq (W := coprod.{v, u} X X) (coprod.desc f₀ f₁) P.i g h.h

Tactic:
have sq : CommSq (coprod.desc f₀ f₁) P.i g h.h := { }
-- 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 : Fibration g
inst_4 : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h_1 : LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)
P : Cylinder.{v, u} X
left_1 : P.IsGood
h : P.LeftHomotopy (f₀ ≫ g) (f₁ ≫ g)
sq : CommSq (W := coprod.{v, u} X X) (coprod.desc f₀ f₁) P.i g h.h
left : LeftHomotopyRel f₀ f₁
⊢ Eq (α := LeftHomotopyClass X Y) (mk f₀) (mk f₁)

Tactic:
rw [mk_eq_mk_iff]

Premises used: HomotopicalAlgebra.LeftHomotopyClass.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 : IsCofibrant.{v, u} X
g : Y ⟶ Z
inst_3 : Fibration g
inst_4 : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h_1 : LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)
P : Cylinder.{v, u} X
left : P.IsGood
h : P.LeftHomotopy (f₀ ≫ g) (f₁ ≫ g)
sq : CommSq (W := coprod.{v, u} X X) (coprod.desc f₀ f₁) P.i g h.h
⊢ CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (P.i ≫ sq.lift) =
    CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (coprod.desc f₀ f₁)

Tactic:
have := coprod.inl ≫= sq.fac_left
-- 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 : Fibration g
inst_4 : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h_1 : LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)
P : Cylinder.{v, u} X
left : P.IsGood
h : P.LeftHomotopy (f₀ ≫ g) (f₁ ≫ g)
sq : CommSq (W := coprod.{v, u} X X) (coprod.desc f₀ f₁) P.i g h.h
this :
  CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (P.i ≫ sq.lift) =
    CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (coprod.desc f₀ f₁)
rwa :
  ∀ (this : P.i₀ ≫ sq.lift = CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (coprod.desc f₀ f₁)),
    P.i₀ ≫ sq.lift = f₀
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : P.i₀ ≫ sq.lift = f₀), P.i₀ ≫ sq.lift = f₀
⊢ P.i₀ ≫ sq.lift = f₀

Tactic:
rwa [P.inl_i_assoc, coprod.inl_desc] at this

Premises used: HomotopicalAlgebra.Cylinder.toPrecylinder, CategoryTheory.Limits.coprod.inl_desc, HomotopicalAlgebra.Precylinder.inl_i_assoc
-- 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 : Fibration g
inst_4 : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h_1 : LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)
P : Cylinder.{v, u} X
left : P.IsGood
h : P.LeftHomotopy (f₀ ≫ g) (f₁ ≫ g)
sq : CommSq (W := coprod.{v, u} X X) (coprod.desc f₀ f₁) P.i g h.h
⊢ CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (P.i ≫ sq.lift) =
    CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (coprod.desc f₀ f₁)

Tactic:
have := coprod.inr ≫= sq.fac_left
-- 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 : Fibration g
inst_4 : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h_1 : LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)
P : Cylinder.{v, u} X
left : P.IsGood
h : P.LeftHomotopy (f₀ ≫ g) (f₁ ≫ g)
sq : CommSq (W := coprod.{v, u} X X) (coprod.desc f₀ f₁) P.i g h.h
this :
  CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (P.i ≫ sq.lift) =
    CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (coprod.desc f₀ f₁)
rwa :
  ∀ (this : P.i₁ ≫ sq.lift = CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (coprod.desc f₀ f₁)),
    P.i₁ ≫ sq.lift = f₁
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : P.i₁ ≫ sq.lift = f₁), P.i₁ ≫ sq.lift = f₁
⊢ P.i₁ ≫ sq.lift = f₁

Tactic:
rwa [P.inr_i_assoc, coprod.inr_desc] at this

Premises used: HomotopicalAlgebra.Precylinder.inr_i_assoc, HomotopicalAlgebra.Cylinder.toPrecylinder, CategoryTheory.Limits.coprod.inr_desc
-- 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 : Fibration g
inst_4 : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h_1 : LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)
P : Cylinder.{v, u} X
left : P.IsGood
h : P.LeftHomotopy (f₀ ≫ g) (f₁ ≫ g)
sq : CommSq (W := coprod.{v, u} X X) (coprod.desc f₀ f₁) P.i g h.h
⊢ LeftHomotopyRel f₀ f₁

Tactic:
exact ⟨P,
      ⟨{h := sq.lift
        h₀ := by
          have := coprod.inl ≫= sq.fac_left
          rwa [P.inl_i_assoc, coprod.inl_desc] at this
        h₁ := by
          have := coprod.inr ≫= sq.fac_left
          rwa [P.inr_i_assoc, coprod.inr_desc] 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 : IsCofibrant.{v, u} X
g : Y ⟶ Z
inst_3 : Fibration g
inst_4 : WeakEquivalence g
φ : LeftHomotopyClass X Z
right :
  ∀ (φ : X ⟶ Z),
    ∃ (a : LeftHomotopyClass X Y),
      Eq (α := LeftHomotopyClass X Z) ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) a) (mk φ)
⊢ ∃ (a : LeftHomotopyClass X Y), (fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) a = φ

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 : Fibration g
inst_4 : WeakEquivalence g
φ : X ⟶ Z
⊢ CommSq (W := initial.{v, u} C) (initial.to Y) (initial.to X) g φ

Tactic:
have sq : CommSq (initial.to Y) (initial.to X) g φ := { }
-- 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 : Fibration g
inst_4 : WeakEquivalence g
φ : X ⟶ Z
sq : CommSq (W := initial.{v, u} C) (initial.to Y) (initial.to X) g φ
⊢ Eq (α := LeftHomotopyClass X Z) ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) (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 : IsCofibrant.{v, u} X
g : Y ⟶ Z
inst_3 : Fibration g
inst_4 : WeakEquivalence g
φ : X ⟶ Z
sq : CommSq (W := initial.{v, u} C) (initial.to Y) (initial.to X) g φ
⊢ ∃ (a : LeftHomotopyClass X Y),
    Eq (α := LeftHomotopyClass X Z) ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) 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 : 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)
rw :
  Function.Bijective.{v + 1, 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)))
⊢ 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:
rw [← Function.Bijective.of_comp_iff'
      (postcomp_bijective_of_fibration_of_weakEquivalence X h.r)]

Premises used: HomotopicalAlgebra.FibrantBrownFactorization.r, HomotopicalAlgebra.LeftHomotopyClass.postcomp_bijective_of_fibration_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 : 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.{v + 1, v + 1} (α := LeftHomotopyClass X Y) 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 : 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₁ :
  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
⊢ Function.Bijective.{v + 1, 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)))

Tactic:
convert! Function.bijective_id

Premises used: Function.bijective_id