awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ (IsPathConnected s ∧ ∀ (x : (↑s : Type u_1)) (γ : Path x x), γ.Homotopic (Path.refl x)) ↔
    IsPathConnected s ∧
      ∀ (x : X) (p : Path x x),
        (∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)) →
          ∃ (F : p.Homotopy (Path.refl x)),
            ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
              Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)
have refine_1 : ∀ (h : ∀ (x : (↑s : Type u_1)) (γ : Path x x), γ.Homotopic (Path.refl x)) (x : X) (p : Path x x)
  (hp : ∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)),
  ∃ (F : p.Homotopy (Path.refl x)),
    ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
      Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)
Tactic: refine .and .rfl ⟨fun h x p hp ↦ ?_, fun h x p ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
refine_1 :
  ∀ (h : ∀ (x : (↑s : Type u_1)) (γ : Path x x), γ.Homotopic (Path.refl x)) (x : X) (p : Path x x)
    (hp : ∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)),
    ∃ (F : p.Homotopy (Path.refl x)),
      ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
        Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)
⊢ (IsPathConnected s ∧ ∀ (x : (↑s : Type u_1)) (γ : Path x x), γ.Homotopic (Path.refl x)) ↔
    IsPathConnected s ∧
      ∀ (x : X) (p : Path x x),
        (∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)) →
          ∃ (F : p.Homotopy (Path.refl x)),
            ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
              Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)
have refine_2 : ∀
  (h :
    ∀ (x : X) (p : Path x x),
      (∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)) →
        ∃ (F : p.Homotopy (Path.refl x)),
          ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
            Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X))
  (x : (↑s : Type u_1)) (p : Path x x), p.Homotopic (Path.refl x)
Tactic: refine .and .rfl ⟨fun h x p hp ↦ ?_, fun h x p ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : ∀ (x : (↑s : Type u_1)) (γ : Path x x), γ.Homotopic (Path.refl x)
x : X
p : Path x x
hp : ∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)
⊢ ∃ (F : p.Homotopy (Path.refl x)),
    ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
      Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)
have refine_1 : ∀ (x : { x : X // x ∈ s }) (p : Path (↑x : X) (↑x : X))
  (hp : ∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)),
  ∃ (F : p.Homotopy (Path.refl (↑x : X))),
    ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
      Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)
Tactic: lift x to s using by simpa using hp 0
Cleared hypotheses: x, p, hp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : ∀ (x : (↑s : Type u_1)) (γ : Path x x), γ.Homotopic (Path.refl x)
x : { x : X // x ∈ s }
p : Path (↑x : X) (↑x : X)
hp : ∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)
⊢ ∃ (F : p.Homotopy (Path.refl (↑x : X))),
    ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
      Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)
have refine_1 : ∀
  (F :
    Path.Homotopy
      {
        toFun := fun (t : (↑unitInterval : Type)) ↦
          Subtype.mk (p := fun (x : X) ↦ x ∈ s) ((p : (a : (↑unitInterval : Type)) → X) t) sorry,
        continuous_toFun := sorry, source' := sorry, target' := sorry }
      (Path.refl x)),
  ∃ (F : p.Homotopy (Path.refl (↑x : X))),
    ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
      Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)
Tactic: rcases h x {
      toFun := fun t ↦ ⟨p t, hp t⟩
      source' := by simp
      target' := by simp
    } with ⟨F⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h :
  ∀ (x : X) (p : Path x x),
    (∀ (t : (↑unitInterval : Type)), Membership.mem (α := X) s ((p : (a : (↑unitInterval : Type)) → X) t : X)) →
      ∃ (F : p.Homotopy (Path.refl x)),
        ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
          Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)
x : (↑s : Type u_1)
p : Path x x
⊢ p.Homotopic (Path.refl x)
have refine_2 : ∀ (F : (p.map sorry).Homotopy (Path.refl (↑x : X)))
  (hF :
    ∀ (t : (↑unitInterval : Type) × (↑unitInterval : Type)),
      Membership.mem (α := X) s ((F : (a : (↑unitInterval : Type) × (↑unitInterval : Type)) → X) t : X)),
  p.Homotopic (Path.refl x)
Tactic: rcases h x (p.map continuous_subtype_val) (fun t ↦ (p t).2) with ⟨F, hF⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : trivialCofibrations C i
hp : fibrations C p
⊢ HasLiftingProperty i p
have left : Cofibration i
Tactic: obtain ⟨_, _⟩ := mem_trivialCofibrations_iff i |>.mp hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : trivialCofibrations C i
hp : fibrations C p
left : Cofibration i
⊢ HasLiftingProperty i p
have right : WeakEquivalence i
Tactic: obtain ⟨_, _⟩ := mem_trivialCofibrations_iff i |>.mp hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : trivialCofibrations C i
hp : fibrations C p
left : Cofibration i
right : WeakEquivalence i
⊢ HasLiftingProperty i p
have hp₁ : Fibration p
Tactic: rw [← fibration_iff] at hp
Cleared hypotheses: hp, left, right
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : cofibrations C i
hp : trivialFibrations C p
⊢ HasLiftingProperty i p
have hp₁ : Fibration p ∧ WeakEquivalence p
Tactic: rw [mem_trivialFibrations_iff] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : cofibrations C i
hp : Fibration p ∧ WeakEquivalence p
⊢ HasLiftingProperty i p
have hi₁ : Cofibration i
Tactic: rw [← cofibration_iff] at hi
Cleared hypotheses: hi, hp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : Cofibration i
hp : Fibration p ∧ WeakEquivalence p
⊢ HasLiftingProperty i p
have this : Fibration p
Tactic: have := hp.1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : Cofibration i
hp : Fibration p ∧ WeakEquivalence p
this : Fibration p
⊢ HasLiftingProperty i p
have this₁ : WeakEquivalence p
Tactic: have := hp.2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
⊢ WeakEquivalence f
have have : ∀ (hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w), WeakEquivalence f
Tactic: have hw := factorizationData (trivialCofibrations C) (fibrations C) w
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w
⊢ IsStableUnderRetracts.{v, u} (trivialFibrations C)
have rw : IsStableUnderRetracts.{v, u} (rlp (cofibrations C))
Tactic: rw [← cofibrations_rlp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w
⊢ WeakEquivalence f
have this : IsStableUnderRetracts.{v, u} (trivialFibrations C)
Tactic: have : (trivialFibrations C).IsStableUnderRetracts := by
    rw [← cofibrations_rlp]
    infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w
this : IsStableUnderRetracts.{v, u} (trivialFibrations C)
⊢ WeakEquivalence f
have sq : CommSq (Arrow.Hom.left h.r) (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f
  (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.r)
Tactic: have sq : CommSq h.r.left hw.i f (hw.p ≫ h.r.right) := ⟨by simp⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w
this : IsStableUnderRetracts.{v, u} (trivialFibrations C)
sq :
  CommSq (Arrow.Hom.left h.r) (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f
    (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.r)
⊢ WeakEquivalence f
have hf : fibrations C f
Tactic: have hf : fibrations C f := by rwa [← fibration_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w
this : IsStableUnderRetracts.{v, u} (trivialFibrations C)
sq :
  CommSq (Arrow.Hom.left h.r) (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f
    (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.r)
hf : fibrations C f
⊢ WeakEquivalence f
have this₁ : HasLiftingProperty (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f
Tactic: have : HasLiftingProperty hw.i f := hasLiftingProperty_of_wfs _ _ hw.hi hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w
this_1 : IsStableUnderRetracts.{v, u} (trivialFibrations C)
sq :
  CommSq (Arrow.Hom.left h.r) (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f
    (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.r)
hf : fibrations C f
this : HasLiftingProperty (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f
⊢ WeakEquivalence f
have have : ∀ (this : RetractArrow f (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))), WeakEquivalence f
Tactic: have : RetractArrow f hw.p :=
    { i := Arrow.homMk (h.i.left ≫ hw.i) h.i.right
      r := Arrow.homMk sq.lift h.r.right }
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w
this_1 : IsStableUnderRetracts.{v, u} (trivialFibrations C)
sq :
  CommSq (Arrow.Hom.left h.r) (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f
    (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.r)
hf : fibrations C f
this_2 : HasLiftingProperty (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f
this : RetractArrow f (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ WeakEquivalence f
have h' : trivialFibrations C (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
Tactic: have h' : trivialFibrations C hw.p :=
    ⟨hw.hp, (weakEquivalence_iff _).1 (weakEquivalence_of_precomp_of_fac hw.fac)⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : weakEquivalences C w
⊢ weakEquivalences C f
have hw₁ : WeakEquivalence w
Tactic: rw [← weakEquivalence_iff] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
⊢ weakEquivalences C f
have have : ∀ (hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f), weakEquivalences C f
Tactic: have hf := factorizationData (trivialCofibrations C) (fibrations C) f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
⊢ weakEquivalences C f
have this : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
Tactic: have : Cofibration hf.i := by
      simpa only [cofibration_iff] using hf.hi.1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ weakEquivalences C f
have this₁ : WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
Tactic: have : WeakEquivalence hf.i := by
      simpa only [weakEquivalence_iff] using hf.hi.2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this_1 : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this : WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
φ : pushout (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ⟶ Y :=
  pushout.desc (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.i) w ⋯
⊢ weakEquivalences C f
have this₁ : Fibration (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
Tactic: have : Fibration hf.p := by simpa only [fibration_iff] using hf.hp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this_1 : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_2 : WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
φ : pushout (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ⟶ Y :=
  pushout.desc (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.i) w ⋯
this : Fibration (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ weakEquivalences C f
have this₁ : WeakEquivalence (pushout.inr (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ≫ φ)
Tactic: have : WeakEquivalence (pushout.inr _ _ ≫ φ) := by simpa [φ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this_1 : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_2 : WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
φ : pushout (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ⟶ Y :=
  pushout.desc (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.i) w ⋯
this_3 : Fibration (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this : WeakEquivalence (pushout.inr (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ≫ φ)
⊢ weakEquivalences C f
have this₁ : WeakEquivalence φ
Tactic: have := weakEquivalence_of_precomp (pushout.inr _ _) φ