awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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₁)
⊢ mk f₀ = f₁
have 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₁)
Tactic: obtain ⟨f₁, rfl⟩ := f₁.mk_surjective
Cleared hypotheses: f₁, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (hypothesis)
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₁))
⊢ Eq (α := LeftHomotopyClass X Y) (mk f₀) (mk f₁)
have h₁ : LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)
Tactic: simp only [postcomp_mk, mk_eq_mk_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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)
⊢ Eq (α := LeftHomotopyClass X Y) (mk f₀) (mk f₁)
have left : ∀ (P : Cylinder.{v, u} X),
  P.IsGood → ∀ (h : P.LeftHomotopy (f₀ ≫ g) (f₁ ≫ g)), Eq (α := LeftHomotopyClass X Y) (mk f₀) (mk f₁)
Tactic: obtain ⟨P, _, ⟨h⟩⟩ := h.exists_good_cylinder
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (hypothesis)
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)
⊢ Eq (α := LeftHomotopyClass X Y) (mk f₀) (mk f₁)
have sq : 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 := { }
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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
⊢ Eq (α := LeftHomotopyClass X Y) (mk f₀) (mk f₁)
have left : LeftHomotopyRel f₀ f₁
Tactic: rw [mk_eq_mk_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (hypothesis)
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
⊢ P.i₀ ≫ sq.lift = f₀
have 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₁)
Tactic: have := coprod.inl ≫= sq.fac_left
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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₁)
⊢ P.i₀ ≫ sq.lift = f₀
have 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₀
Tactic: rwa [P.inl_i_assoc, coprod.inl_desc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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₀
⊢ P.i₀ ≫ sq.lift = f₀
have rwa₁ : ∀ (this : P.i₀ ≫ sq.lift = f₀), P.i₀ ≫ sq.lift = f₀
Tactic: rwa [P.inl_i_assoc, coprod.inl_desc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (hypothesis)
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
⊢ P.i₁ ≫ sq.lift = f₁
have 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₁)
Tactic: have := coprod.inr ≫= sq.fac_left
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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₁)
⊢ P.i₁ ≫ sq.lift = f₁
have 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₁
Tactic: rwa [P.inr_i_assoc, coprod.inr_desc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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₁
⊢ P.i₁ ≫ sq.lift = f₁
have rwa₁ : ∀ (this : P.i₁ ≫ sq.lift = f₁), P.i₁ ≫ sq.lift = f₁
Tactic: rwa [P.inr_i_assoc, coprod.inr_desc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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
⊢ ∃ (a : LeftHomotopyClass X Y), (fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) a = φ
have right : ∀ (φ : X ⟶ Z),
  ∃ (a : LeftHomotopyClass X Y),
    Eq (α := LeftHomotopyClass X Z) ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) a) (mk φ)
Tactic: obtain ⟨φ, rfl⟩ := φ.mk_surjective
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (hypothesis)
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
⊢ ∃ (a : LeftHomotopyClass X Y),
    Eq (α := LeftHomotopyClass X Z) ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) a) (mk φ)
have sq : CommSq (W := initial.{v, u} C) (initial.to Y) (initial.to X) g φ
Tactic: have sq : CommSq (initial.to Y) (initial.to X) g φ := { }
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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))
have 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)))
Tactic: rw [← Function.Bijective.of_comp_iff'
      (postcomp_bijective_of_fibration_of_weakEquivalence X h.r)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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) (β := 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)))
have 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
Tactic: convert! Function.bijective_id
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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)
⊢ 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
have 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 φ
Tactic: ext φ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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
⊢ ((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 φ
have 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 φ))
Tactic: obtain ⟨φ, rfl⟩ := φ.mk_surjective
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (hypothesis)
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 Z) fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g
have 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))
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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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 (β := LeftHomotopyClass X Z) fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g
have 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)))
Tactic: convert! (postcomp_bijective_of_fibration_of_weakEquivalence X h.p).comp hi using 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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))
⊢ 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)))
have 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)))
      φ
Tactic: ext φ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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
⊢ φ.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)))
      φ
have 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 φ))
Tactic: obtain ⟨φ, rfl⟩ := φ.mk_surjective
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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
⊢ Function.Bijective (β := RightHomotopyClass X Z) fun (g : RightHomotopyClass Y Z) ↦ g.precomp f
have left : Function.Injective (β := RightHomotopyClass X Z) fun (g : RightHomotopyClass Y Z) ↦ g.precomp f
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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
⊢ Function.Bijective (β := RightHomotopyClass X Z) fun (g : RightHomotopyClass Y Z) ↦ g.precomp f
have right : Function.Surjective (β := RightHomotopyClass X Z) fun (g : RightHomotopyClass Y Z) ↦ g.precomp f
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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₁)
⊢ f₀ = f₁
have 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₁
Tactic: obtain ⟨f₀, rfl⟩ := f₀.mk_surjective
Cleared hypotheses: f₀, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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₁)
⊢ mk f₀ = f₁
have 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₁)
Tactic: obtain ⟨f₁, rfl⟩ := f₁.mk_surjective
Cleared hypotheses: f₁, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (hypothesis)
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₁))
⊢ Eq (α := RightHomotopyClass Y Z) (mk f₀) (mk f₁)
have h₁ : RightHomotopyRel (f ≫ f₀) (f ≫ f₁)
Tactic: simp only [precomp_mk, mk_eq_mk_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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₁)
⊢ Eq (α := RightHomotopyClass Y Z) (mk f₀) (mk f₁)
have left : ∀ (P : PathObject.{v, u} Z),
  P.IsGood → ∀ (h : P.RightHomotopy (f ≫ f₀) (f ≫ f₁)), Eq (α := RightHomotopyClass Y Z) (mk f₀) (mk f₁)
Tactic: obtain ⟨P, _, ⟨h⟩⟩ := h.exists_good_pathObject
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (hypothesis)
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₁)
⊢ Eq (α := RightHomotopyClass Y Z) (mk f₀) (mk f₁)
have sq : 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₁) := { }
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
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₁)
⊢ Eq (α := RightHomotopyClass Y Z) (mk f₀) (mk f₁)
have left : RightHomotopyRel f₀ f₁
Tactic: rw [mk_eq_mk_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (hypothesis)
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₁)
⊢ sq.lift ≫ P.p₀ = f₀
have 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
Tactic: have := sq.fac_right =≫ prod.fst