awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : CofibrantBrownFactorization f
inst_2 : IsCofibrant.{v_1, u_1} X
inst_3 : IsCofibrant.{v_1, u_1} Y
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := coprod.{v_1, u_1} X Y) (coprod.desc f (𝟙 Y))
⊢ WeakEquivalence (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : CofibrantBrownFactorization f
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := coprod.{v_1, u_1} X Y) (coprod.desc f (𝟙 Y))
inst_2 : IsCofibrant.{v_1, u_1} X
inst_3 : IsCofibrant.{v_1, u_1} Y
⊢ Nonempty (CofibrantBrownFactorization f)

Tactic:
⟨.mk' f (MorphismProperty.factorizationData _ _ _)⟩

Premises used: CategoryTheory.MorphismProperty.factorizationData, HomotopicalAlgebra.CofibrantBrownFactorization.mk', Nonempty.intro
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h : FibrantBrownFactorization f
inst_2 : WeakEquivalence f
⊢ WeakEquivalence (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
weakEquivalence_of_precomp_of_fac h.fac

Premises used: CategoryTheory.MorphismProperty.MapFactorizationData.fac, HomotopicalAlgebra.FibrantBrownFactorization.toMapFactorizationData, HomotopicalAlgebra.weakEquivalence_of_precomp_of_fac
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h : FibrantBrownFactorization f
⊢ WeakEquivalence h.r

Tactic:
weakEquivalence_of_precomp_of_fac h.i_r

Premises used: HomotopicalAlgebra.FibrantBrownFactorization.i_r, HomotopicalAlgebra.weakEquivalence_of_precomp_of_fac
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : FibrantBrownFactorization f
inst_2 : IsFibrant.{v_1, u_1} X
inst_3 : IsFibrant.{v_1, u_1} Y
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v_1, u_1} Y X) (prod.lift f (𝟙 X))
rw :
  Cofibration (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) ∧
    WeakEquivalence (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ trivialCofibrations C (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
rw [mem_trivialCofibrations_iff]

Premises used: HomotopicalAlgebra.mem_trivialCofibrations_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : FibrantBrownFactorization f
inst_2 : IsFibrant.{v_1, u_1} X
inst_3 : IsFibrant.{v_1, u_1} Y
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v_1, u_1} Y X) (prod.lift f (𝟙 X))
left : Cofibration (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
right : WeakEquivalence (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ Cofibration (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) ∧
    WeakEquivalence (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : FibrantBrownFactorization f
inst_2 : IsFibrant.{v_1, u_1} X
inst_3 : IsFibrant.{v_1, u_1} Y
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v_1, u_1} Y X) (prod.lift f (𝟙 X))
⊢ Cofibration (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : FibrantBrownFactorization f
inst_2 : IsFibrant.{v_1, u_1} X
inst_3 : IsFibrant.{v_1, u_1} Y
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v_1, u_1} Y X) (prod.lift f (𝟙 X))
⊢ WeakEquivalence (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : FibrantBrownFactorization f
inst_2 : IsFibrant.{v_1, u_1} X
inst_3 : IsFibrant.{v_1, u_1} Y
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v_1, u_1} Y X) (prod.lift f (𝟙 X))
rw : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.fst)
⊢ fibrations C (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.fst)

Tactic:
rw [← fibration_iff]

Premises used: HomotopicalAlgebra.fibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : FibrantBrownFactorization f
inst_2 : IsFibrant.{v_1, u_1} X
inst_3 : IsFibrant.{v_1, u_1} Y
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v_1, u_1} Y X) (prod.lift f (𝟙 X))
⊢ Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.fst)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h : FibrantBrownFactorization f
inst_2 : IsFibrant.{v_1, u_1} X
inst_3 : IsFibrant.{v_1, u_1} Y
⊢ Nonempty (FibrantBrownFactorization f)

Tactic:
⟨.mk' f (MorphismProperty.factorizationData _ _ _)⟩

Premises used: CategoryTheory.MorphismProperty.factorizationData, Nonempty.intro, HomotopicalAlgebra.FibrantBrownFactorization.mk'
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : Fibration f
⊢ fibrations C f

Tactic:
Fibration.mem

Premises used: HomotopicalAlgebra.Fibration.mem
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithCofibrations.{v, u} C
inst_2 : Cofibration f
⊢ cofibrations C f

Tactic:
Cofibration.mem

Premises used: HomotopicalAlgebra.Cofibration.mem
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : WeakEquivalence f
⊢ weakEquivalences C f

Tactic:
WeakEquivalence.mem

Premises used: HomotopicalAlgebra.WeakEquivalence.mem
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithWeakEquivalences.{v, u} C
⊢ LE.le (α := MorphismProperty.{v, u} C) (trivialFibrations C) (fibrations C)

Tactic:
fun _ _ _ hf ↦ hf.1

Premises used: And.left
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithWeakEquivalences.{v, u} C
⊢ LE.le (α := MorphismProperty.{v, u} C) (trivialFibrations C) (weakEquivalences C)

Tactic:
fun _ _ _ hf ↦ hf.2

Premises used: And.right
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithWeakEquivalences.{v, u} C
inst_3 : Fibration f
inst_4 : WeakEquivalence f
⊢ trivialFibrations C f

Tactic:
⟨mem_fibrations f, mem_weakEquivalences f⟩

Premises used: HomotopicalAlgebra.mem_fibrations, HomotopicalAlgebra.mem_weakEquivalences, And.intro, HomotopicalAlgebra.trivialFibrations
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithWeakEquivalences.{v, u} C
rw : trivialFibrations C f ↔ fibrations C f ∧ weakEquivalences C f
⊢ trivialFibrations C f ↔ Fibration f ∧ WeakEquivalence f

Tactic:
rw [fibration_iff, weakEquivalence_iff]

Premises used: HomotopicalAlgebra.fibration_iff, HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithWeakEquivalences.{v, u} C
⊢ trivialFibrations C f ↔ fibrations C f ∧ weakEquivalences C f

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithCofibrations.{v, u} C
inst_2 : CategoryWithWeakEquivalences.{v, u} C
⊢ LE.le (α := MorphismProperty.{v, u} C) (trivialCofibrations C) (cofibrations C)

Tactic:
fun _ _ _ hf ↦ hf.1

Premises used: And.left
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithCofibrations.{v, u} C
inst_2 : CategoryWithWeakEquivalences.{v, u} C
⊢ LE.le (α := MorphismProperty.{v, u} C) (trivialCofibrations C) (weakEquivalences C)

Tactic:
fun _ _ _ hf ↦ hf.2

Premises used: And.right
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithCofibrations.{v, u} C
inst_2 : CategoryWithWeakEquivalences.{v, u} C
inst_3 : Cofibration f
inst_4 : WeakEquivalence f
⊢ trivialCofibrations C f

Tactic:
⟨mem_cofibrations f, mem_weakEquivalences f⟩

Premises used: HomotopicalAlgebra.mem_cofibrations, HomotopicalAlgebra.mem_weakEquivalences, And.intro, HomotopicalAlgebra.trivialCofibrations
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithCofibrations.{v, u} C
inst_2 : CategoryWithWeakEquivalences.{v, u} C
rw : trivialCofibrations C f ↔ cofibrations C f ∧ weakEquivalences C f
⊢ trivialCofibrations C f ↔ Cofibration f ∧ WeakEquivalence f

Tactic:
rw [cofibration_iff, weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff, HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithCofibrations.{v, u} C
inst_2 : CategoryWithWeakEquivalences.{v, u} C
⊢ trivialCofibrations C f ↔ cofibrations C f ∧ weakEquivalences C f

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithCofibrations.{v, u} C
⊢ Eq (α := MorphismProperty.{v, u} Cᵒᵖ) (fibrations Cᵒᵖ) (MorphismProperty.op (cofibrations C))

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.op, HomotopicalAlgebra.cofibrations, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithCofibrations.{v, u} C
⊢ Eq (α := MorphismProperty.{v, u} C) (cofibrations C) (MorphismProperty.unop (fibrations Cᵒᵖ))

Tactic:
rfl

Premises used: HomotopicalAlgebra.fibrations, CategoryTheory.MorphismProperty.unop, Quiver.Hom.unop, CategoryTheory.MorphismProperty.op, HomotopicalAlgebra.cofibrations, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithCofibrations.{v, u} C
⊢ Fibration.{v, u} (C := Cᵒᵖ) (X := Opposite.op Y) (Y := Opposite.op X) f.op ↔ Cofibration f

Tactic:
simp [cofibration_iff, fibration_iff, cofibrations_eq_unop]

Premises used: HomotopicalAlgebra.fibration_iff, HomotopicalAlgebra.cofibrations_eq_unop, HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithCofibrations.{v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ Cofibration f.unop ↔ Fibration.{v, u} (C := Cᵒᵖ) (X := X) (Y := Y) f

Tactic:
simp [cofibration_iff, fibration_iff, cofibrations_eq_unop]

Premises used: HomotopicalAlgebra.fibration_iff, HomotopicalAlgebra.cofibrations_eq_unop, HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithCofibrations.{v, u} C
inst_2 rwa rwa₁ rwa₂ rwa₃ : Cofibration f
⊢ Fibration.{v, u} (C := Cᵒᵖ) (X := Opposite.op Y) (Y := Opposite.op X) f.op

Tactic:
rwa [fibration_op_iff]

Premises used: HomotopicalAlgebra.fibration_op_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_1 : CategoryWithCofibrations.{v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst_2 rwa rwa₁ rwa₂ rwa₃ : Fibration.{v, u} (C := Cᵒᵖ) (X := X) (Y := Y) f
⊢ Cofibration f.unop

Tactic:
rwa [cofibration_unop_iff]

Premises used: HomotopicalAlgebra.cofibration_unop_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
⊢ Eq (α := MorphismProperty.{v, u} Cᵒᵖ) (cofibrations Cᵒᵖ) (MorphismProperty.op (fibrations C))

Tactic:
rfl

Premises used: HomotopicalAlgebra.fibrations, CategoryTheory.MorphismProperty.op, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
⊢ Eq (α := MorphismProperty.{v, u} C) (fibrations C) (MorphismProperty.unop (cofibrations Cᵒᵖ))

Tactic:
rfl

Premises used: HomotopicalAlgebra.fibrations, CategoryTheory.MorphismProperty.unop, Quiver.Hom.unop, CategoryTheory.MorphismProperty.op, HomotopicalAlgebra.cofibrations, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithFibrations.{v, u} C
⊢ Cofibration.{v, u} (C := Cᵒᵖ) (X := Opposite.op Y) (Y := Opposite.op X) f.op ↔ Fibration f

Tactic:
simp [cofibration_iff, fibration_iff, fibrations_eq_unop]

Premises used: HomotopicalAlgebra.fibration_iff, HomotopicalAlgebra.fibrations_eq_unop, HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ Fibration f.unop ↔ Cofibration.{v, u} (C := Cᵒᵖ) (X := X) (Y := Y) f

Tactic:
simp [cofibration_iff, fibration_iff, fibrations_eq_unop]

Premises used: HomotopicalAlgebra.fibration_iff, HomotopicalAlgebra.fibrations_eq_unop, HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 rwa rwa₁ rwa₂ rwa₃ : Fibration f
⊢ Cofibration.{v, u} (C := Cᵒᵖ) (X := Opposite.op Y) (Y := Opposite.op X) f.op

Tactic:
rwa [cofibration_op_iff]

Premises used: HomotopicalAlgebra.cofibration_op_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_1 : CategoryWithFibrations.{v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst_2 rwa rwa₁ rwa₂ rwa₃ : Cofibration.{v, u} (C := Cᵒᵖ) (X := X) (Y := Y) f
⊢ Fibration f.unop

Tactic:
rwa [fibration_unop_iff]

Premises used: HomotopicalAlgebra.fibration_unop_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
⊢ Eq (α := MorphismProperty.{v, u} Cᵒᵖ) (weakEquivalences Cᵒᵖ) (MorphismProperty.op (weakEquivalences C))

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.op, HomotopicalAlgebra.weakEquivalences, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
⊢ Eq (α := MorphismProperty.{v, u} C) (weakEquivalences C) (MorphismProperty.unop (weakEquivalences Cᵒᵖ))

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.unop, Quiver.Hom.unop, CategoryTheory.MorphismProperty.op, HomotopicalAlgebra.weakEquivalences, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithWeakEquivalences.{v, u} C
⊢ WeakEquivalence.{v, u} (C := Cᵒᵖ) (X := Opposite.op Y) (Y := Opposite.op X) f.op ↔ WeakEquivalence f

Tactic:
simp [weakEquivalence_iff, weakEquivalences_op]

Premises used: HomotopicalAlgebra.weakEquivalences_op, HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ WeakEquivalence f.unop ↔ WeakEquivalence.{v, u} (C := Cᵒᵖ) (X := X) (Y := Y) f

Tactic:
(weakEquivalences_op_iff f.unop).symm

Premises used: Quiver.Hom.op, HomotopicalAlgebra.weakEquivalences_op_iff, Quiver.Hom.unop, Iff.symm
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 rwa rwa₁ rwa₂ rwa₃ : WeakEquivalence f
⊢ WeakEquivalence.{v, u} (C := Cᵒᵖ) (X := Opposite.op Y) (Y := Opposite.op X) f.op

Tactic:
rwa [weakEquivalences_op_iff]

Premises used: HomotopicalAlgebra.weakEquivalences_op_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst_2 rwa rwa₁ rwa₂ rwa₃ : WeakEquivalence.{v, u} (C := Cᵒᵖ) (X := X) (Y := Y) f
⊢ WeakEquivalence f.unop

Tactic:
rwa [weakEquivalences_unop_iff]

Premises used: HomotopicalAlgebra.weakEquivalences_unop_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
⊢ Eq (α := MorphismProperty.{v, u} Cᵒᵖ) (trivialFibrations Cᵒᵖ) (MorphismProperty.op (trivialCofibrations C))

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.op, HomotopicalAlgebra.cofibrations, HomotopicalAlgebra.trivialFibrations, HomotopicalAlgebra.weakEquivalences, rfl, HomotopicalAlgebra.trivialCofibrations
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
⊢ Eq (α := MorphismProperty.{v, u} C) (trivialCofibrations C) (MorphismProperty.unop (trivialFibrations Cᵒᵖ))

Tactic:
rfl

Premises used: HomotopicalAlgebra.fibrations, CategoryTheory.MorphismProperty.unop, Quiver.Hom.unop, CategoryTheory.MorphismProperty.op, HomotopicalAlgebra.cofibrations, HomotopicalAlgebra.trivialFibrations, HomotopicalAlgebra.weakEquivalences, rfl, HomotopicalAlgebra.trivialCofibrations
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithFibrations.{v, u} C
⊢ Eq (α := MorphismProperty.{v, u} Cᵒᵖ) (trivialCofibrations Cᵒᵖ) (MorphismProperty.op (trivialFibrations C))

Tactic:
rfl

Premises used: HomotopicalAlgebra.fibrations, CategoryTheory.MorphismProperty.op, HomotopicalAlgebra.trivialFibrations, HomotopicalAlgebra.weakEquivalences, rfl, HomotopicalAlgebra.trivialCofibrations
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithFibrations.{v, u} C
⊢ Eq (α := MorphismProperty.{v, u} C) (trivialFibrations C) (MorphismProperty.unop (trivialCofibrations Cᵒᵖ))

Tactic:
rfl

Premises used: HomotopicalAlgebra.fibrations, CategoryTheory.MorphismProperty.unop, Quiver.Hom.unop, CategoryTheory.MorphismProperty.op, HomotopicalAlgebra.cofibrations, HomotopicalAlgebra.trivialFibrations, HomotopicalAlgebra.weakEquivalences, rfl, HomotopicalAlgebra.trivialCofibrations
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
⊢ MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (C := P.FullSubcategory) (weakEquivalences P.FullSubcategory)

Tactic:
inferInstanceAs ((weakEquivalences C).inverseImage P.ι).HasTwoOutOfThreeProperty

Premises used: _private.0.HomotopicalAlgebra.instHasTwoOutOfThreePropertyFullSubcategoryWeakEquivalences._proof_1
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : MorphismProperty.IsMultiplicative.{v, u} (weakEquivalences C)
⊢ MorphismProperty.IsMultiplicative.{v, u} (C := P.FullSubcategory) (weakEquivalences P.FullSubcategory)

Tactic:
inferInstanceAs ((weakEquivalences C).inverseImage P.ι).IsMultiplicative

Premises used: _private.0.HomotopicalAlgebra.instIsMultiplicativeFullSubcategoryWeakEquivalences._proof_1
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
f : X ⟶ Y
simp : weakEquivalences P.FullSubcategory f ↔ weakEquivalences C f.hom
⊢ WeakEquivalence f ↔ WeakEquivalence f.hom

Tactic:
simp only [weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
f : X ⟶ Y
⊢ weakEquivalences P.FullSubcategory f ↔ weakEquivalences C f.hom

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
f : X ⟶ Y
inst_2 rwa rwa₁ rwa₂ rwa₃ : WeakEquivalence f
⊢ WeakEquivalence f.hom

Tactic:
rwa [← weakEquivalence_iff_of_objectProperty]

Premises used: HomotopicalAlgebra.weakEquivalence_iff_of_objectProperty
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
f : X ⟶ Y
inst_2 : WeakEquivalence f
dsimp : WeakEquivalence f.hom
⊢ WeakEquivalence (P.ι.map f)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
f : X ⟶ Y
inst_2 : WeakEquivalence f
⊢ WeakEquivalence f.hom

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
⊢ homRel C f g ↔ RightHomotopyRel f.hom g.hom

Tactic:
Iff.rfl

Premises used: Iff.rfl, HomotopicalAlgebra.CofibrantObject.homRel