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 : 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
⊢ sq.lift ≫ P.p₀ = f₀
have 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₀
Tactic: rwa [Category.assoc, P.p_fst, prod.lift_fst] 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 : 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₀
⊢ sq.lift ≫ P.p₀ = f₀
have 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₀
Tactic: rwa [Category.assoc, P.p_fst, prod.lift_fst] 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 : 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₀
⊢ sq.lift ≫ P.p₀ = f₀
have rwa₂ : ∀ (this : sq.lift ≫ P.p₀ = f₀), sq.lift ≫ P.p₀ = f₀
Tactic: rwa [Category.assoc, P.p_fst, prod.lift_fst] 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 : 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.snd =
  CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift f₀ f₁) prod.snd
Tactic: have := sq.fac_right =≫ prod.snd
-- 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₁)
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
⊢ sq.lift ≫ P.p₁ = f₁
have 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₁
Tactic: rwa [Category.assoc, P.p_snd, prod.lift_snd] 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 : 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₁
⊢ sq.lift ≫ P.p₁ = f₁
have 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₁
Tactic: rwa [Category.assoc, P.p_snd, prod.lift_snd] 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 : 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₁
⊢ sq.lift ≫ P.p₁ = f₁
have rwa₂ : ∀ (this : sq.lift ≫ P.p₁ = f₁), sq.lift ≫ P.p₁ = f₁
Tactic: rwa [Category.assoc, P.p_snd, prod.lift_snd] 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 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
φ : RightHomotopyClass X Z
⊢ ∃ (a : RightHomotopyClass Y Z), (fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) a = φ
have right : ∀ (φ : X ⟶ Z),
  ∃ (a : RightHomotopyClass Y Z),
    Eq (α := RightHomotopyClass X Z) ((fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) 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 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
φ : X ⟶ Z
⊢ ∃ (a : RightHomotopyClass Y Z),
    Eq (α := RightHomotopyClass X Z) ((fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) a) (mk φ)
have sq : CommSq (Z := terminal.{v, u} C) φ f (terminal.from Z) (terminal.from Y)
Tactic: have sq : CommSq φ f (terminal.from _) (terminal.from _) := { }
-- 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 : IsCofibrant.{v, u} X
inst_4 : IsCofibrant.{v, u} Y
inst_5 : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
⊢ 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))
have 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)))
Tactic: rw [← Function.Bijective.of_comp_iff'
      (precomp_bijective_of_cofibration_of_weakEquivalence Z h.s)]
-- 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 : 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) (β := 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)))
have 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
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 : 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)
⊢ 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
have h₁ : ∀ (φ : 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 φ
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 : 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)
φ : 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 φ
have h₁ : ∀ (φ : Y ⟶ Z),
  Eq (α := 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)))
      (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 : 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 (β := RightHomotopyClass X Z) fun (g : RightHomotopyClass Y Z) ↦ g.precomp f
have hj : 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: have hj : Function.Bijective (fun (g : RightHomotopyClass Y Z) ↦ g.precomp h.p) := by
    rw [← Function.Bijective.of_comp_iff'
      (precomp_bijective_of_cofibration_of_weakEquivalence Z h.s)]
    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 : 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)
hj :
  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))
⊢ Function.Bijective (β := RightHomotopyClass X Z) fun (g : RightHomotopyClass Y Z) ↦ g.precomp f
have h₁ : Eq.{v + 1} (α := RightHomotopyClass Y Z → RightHomotopyClass X Z) (fun (g : RightHomotopyClass Y Z) ↦ g.precomp f)
  ((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦
      g.precomp (h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))) ∘
    fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))
Tactic: convert! (precomp_bijective_of_cofibration_of_weakEquivalence Z h.i).comp hj 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 : 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)
hj :
  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))
⊢ Eq.{v + 1} (α := RightHomotopyClass Y Z → RightHomotopyClass X Z) (fun (g : RightHomotopyClass Y Z) ↦ g.precomp f)
    ((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦
        g.precomp (h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))) ∘
      fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))
have h₁ : ∀ (φ : RightHomotopyClass Y Z),
  φ.precomp f =
    ((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦
          g.precomp (h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))) ∘
        fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations 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 : 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)
hj :
  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))
φ : RightHomotopyClass Y Z
⊢ φ.precomp f =
    ((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦
          g.precomp (h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))) ∘
        fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))
      φ
have h₁ : ∀ (φ : Y ⟶ Z),
  Eq (α := RightHomotopyClass X Z) (precomp (mk φ) f)
    (((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦
          g.precomp (h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))) ∘
        fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations 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 : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
⊢ ∃ (g : Y ⟶ X), RightHomotopyRel (f ≫ g) (𝟙 X) ∧ RightHomotopyRel (g ≫ f) (𝟙 Y)
have obtain : ∀ (g : RightHomotopyClass Y X)
  (hg : Eq.{v + 1} (α := RightHomotopyClass X X) ((fun (g : RightHomotopyClass Y X) ↦ g.precomp f) g) (mk (𝟙 X))),
  ∃ (g : Y ⟶ X), RightHomotopyRel (f ≫ g) (𝟙 X) ∧ RightHomotopyRel (g ≫ f) (𝟙 Y)
Tactic: obtain ⟨g, hg⟩ := (precomp_bijective_of_weakEquivalence X f).2 (.mk (𝟙 X))
-- 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 : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
g : RightHomotopyClass Y X
hg : Eq.{v + 1} (α := RightHomotopyClass X X) ((fun (g : RightHomotopyClass Y X) ↦ g.precomp f) g) (mk (𝟙 X))
⊢ ∃ (g : Y ⟶ X), RightHomotopyRel (f ≫ g) (𝟙 X) ∧ RightHomotopyRel (g ≫ f) (𝟙 Y)
have obtain : ∀ (g : Y ⟶ X)
  (hg : Eq.{v + 1} (α := RightHomotopyClass X X) ((fun (g : RightHomotopyClass Y X) ↦ g.precomp f) (mk g)) (mk (𝟙 X))),
  ∃ (g : Y ⟶ X), RightHomotopyRel (f ≫ g) (𝟙 X) ∧ RightHomotopyRel (g ≫ f) (𝟙 Y)
Tactic: obtain ⟨g, rfl⟩ := g.mk_surjective
Cleared hypotheses: g, hg
-- 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 : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
g : Y ⟶ X
hg : Eq (α := RightHomotopyClass X X) (mk (f ≫ g)) (mk (𝟙 X))
⊢ ∃ (g : Y ⟶ X), RightHomotopyRel (f ≫ g) (𝟙 X) ∧ RightHomotopyRel (g ≫ f) (𝟙 Y)
have refine : RightHomotopyRel (g ≫ f) (𝟙 Y)
Tactic: refine ⟨g, by rwa [← mk_eq_mk_iff], ?_⟩
-- 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 : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
g : Y ⟶ X
hg : Eq (α := RightHomotopyClass X X) (mk (f ≫ g)) (mk (𝟙 X))
⊢ RightHomotopyRel (g ≫ f) (𝟙 Y)
have rw : Eq (α := RightHomotopyClass Y Y) (mk (g ≫ f)) (mk (𝟙 Y))
Tactic: rw [← mk_eq_mk_iff]
-- 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 : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
g : Y ⟶ X
hg : Eq (α := RightHomotopyClass X X) (mk (f ≫ g)) (mk (𝟙 X))
⊢ Eq (α := RightHomotopyClass Y Y) (mk (g ≫ f)) (mk (𝟙 Y))
have a : Eq.{v + 1} (α := RightHomotopyClass X Y) ((fun (g : RightHomotopyClass Y Y) ↦ g.precomp f) (mk (g ≫ f)))
  ((fun (g : RightHomotopyClass Y Y) ↦ g.precomp f) (mk (𝟙 Y)))
Tactic: apply (precomp_bijective_of_weakEquivalence Y f).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 : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
g : Y ⟶ X
hg : Eq (α := RightHomotopyClass X X) (mk (f ≫ g)) (mk (𝟙 X))
⊢ Eq.{v + 1} (α := RightHomotopyClass X Y) ((fun (g : RightHomotopyClass Y Y) ↦ g.precomp f) (mk (g ≫ f)))
    ((fun (g : RightHomotopyClass Y Y) ↦ g.precomp f) (mk (𝟙 Y)))
have a : Eq (α := RightHomotopyClass X Y) (mk (f ≫ g ≫ f)) (mk f)
Tactic: simp only [precomp_mk, Category.comp_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 : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
g : Y ⟶ X
hg : Eq (α := RightHomotopyClass X X) (mk (f ≫ g)) (mk (𝟙 X))
⊢ Eq (α := RightHomotopyClass X Y) (mk (f ≫ g ≫ f)) (mk f)
have a : ∀ (hg : LeftHomotopyRel (f ≫ g) (𝟙 X)), LeftHomotopyRel (f ≫ g ≫ f) f
Tactic: rw [mk_eq_mk_iff, ← leftHomotopyRel_iff_rightHomotopyRel] at hg ⊢
Cleared hypotheses: hg
-- 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 : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
⊢ ∃ (g : Y ⟶ X), LeftHomotopyRel (f ≫ g) (𝟙 X) ∧ LeftHomotopyRel (g ≫ f) (𝟙 Y)
have simp : ∃ (g : Y ⟶ X), RightHomotopyRel (f ≫ g) (𝟙 X) ∧ RightHomotopyRel (g ≫ f) (𝟙 Y)
Tactic: simp only [leftHomotopyRel_iff_rightHomotopyRel]
-- 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
inst_3 : IsFibrant.{v, u} Y
x x_1 : X ⟶ Y
h : LeftHomotopyRel x x_1
⊢ Eq (α := RightHomotopyClass X Y) (RightHomotopyClass.mk x) (RightHomotopyClass.mk x_1)
have rw : RightHomotopyRel x x_1
Tactic: rw [RightHomotopyClass.mk_eq_mk_iff]
-- 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
inst_3 : IsFibrant.{v, u} Y
x x_1 : X ⟶ Y
h : RightHomotopyRel x x_1
⊢ Eq (α := LeftHomotopyClass X Y) (LeftHomotopyClass.mk x) (LeftHomotopyClass.mk x_1)
have rw : LeftHomotopyRel x x_1
Tactic: rw [LeftHomotopyClass.mk_eq_mk_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : WeakEquivalence g
hfg : WeakEquivalence (f ≫ g)
⊢ WeakEquivalence f
have rw : ∀ (hg : weakEquivalences C g) (hfg : weakEquivalences C (f ≫ g)), weakEquivalences C f
Tactic: rw [weakEquivalence_iff] at hg hfg ⊢
Cleared hypotheses: hg, hfg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : WeakEquivalence f
hfg : WeakEquivalence (f ≫ g)
⊢ WeakEquivalence g
have rw : ∀ (hf : weakEquivalences C f) (hfg : weakEquivalences C (f ≫ g)), weakEquivalences C g
Tactic: rw [weakEquivalence_iff] at hf hfg ⊢
Cleared hypotheses: hf, hfg