awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y : C
inst_4 : IsCofibrant.{v_1, u_1} X
inst_5 : IsFibrant.{v_1, u_1} Y
⊢ Function.Bijective (α := LeftHomotopyClass X Y) (leftHomotopyClassToHom L) ↔
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
have this : Eq (α := LeftHomotopyClass X Y → (L.obj X ⟶ L.obj Y)) (leftHomotopyClassToHom L)
  (Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
    (⇑leftHomotopyClassEquivRightHomotopyClass : (a : LeftHomotopyClass X Y) → RightHomotopyClass X Y))
Tactic: have : (leftHomotopyClassToHom L : LeftHomotopyClass X Y → _) =
      rightHomotopyClassToHom L ∘ leftHomotopyClassEquivRightHomotopyClass := by
    ext f
    obtain ⟨f, rfl⟩ := f.mk_surjective
    simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y : C
inst_4 : IsCofibrant.{v_1, u_1} X
inst_5 : IsFibrant.{v_1, u_1} Y
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
have inr : ∀
  (this :
    ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
      Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)),
  ¬IsCofibrant.{v_1, u_1} Y → Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
Tactic: wlog _ : IsCofibrant Y generalizing Y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y : C
inst_4 : IsCofibrant.{v_1, u_1} X
inst_5 : IsFibrant.{v_1, u_1} Y
inr :
  ∀
    (this :
      ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
        Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)),
    ¬IsCofibrant.{v_1, u_1} Y → Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
have wlog : ∀ (Y : C) [IsFibrant.{v_1, u_1} Y],
  IsCofibrant.{v_1, u_1} Y → Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
Tactic: wlog _ : IsCofibrant Y generalizing Y
Cleared hypotheses: inst_5
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y : C
inst_4 : IsCofibrant.{v_1, u_1} X
inst_5 : IsFibrant.{v_1, u_1} Y
this :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h : ¬IsCofibrant.{v_1, u_1} Y
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
have inr : ∀ (Y' : C),
  IsCofibrant.{v_1, u_1} Y' →
    ∀ (p : Y' ⟶ Y),
      Fibration p → WeakEquivalence p → Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
Tactic: obtain ⟨Y', _, p, _, _⟩ := CofibrantObject.HoCat.exists_resolution Y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y : C
inst_4 : IsCofibrant.{v_1, u_1} X
inst_5 : IsFibrant.{v_1, u_1} Y
this :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h : ¬IsCofibrant.{v_1, u_1} Y
Y' : C
w : IsCofibrant.{v_1, u_1} Y'
p : Y' ⟶ Y
left : Fibration p
right : WeakEquivalence p
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
have x : IsFibrant.{v_1, u_1} Y'
Tactic: have _ : IsFibrant Y' := isFibrant_of_fibration p
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y : C
inst_4 : IsCofibrant.{v_1, u_1} X
inst_5 : IsFibrant.{v_1, u_1} Y
this :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h : ¬IsCofibrant.{v_1, u_1} Y
Y' : C
w : IsCofibrant.{v_1, u_1} Y'
p : Y' ⟶ Y
left : Fibration p
right : WeakEquivalence p
h_1 : IsFibrant.{v_1, u_1} Y'
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
have hY' : Function.Bijective (α := RightHomotopyClass X Y') (rightHomotopyClassToHom L)
Tactic: have hY' := this Y' inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y : C
inst_4 : IsCofibrant.{v_1, u_1} X
inst_5 : IsFibrant.{v_1, u_1} Y
this :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h : ¬IsCofibrant.{v_1, u_1} Y
Y' : C
w : IsCofibrant.{v_1, u_1} Y'
p : Y' ⟶ Y
left : Fibration p
right : WeakEquivalence p
h_1 : IsFibrant.{v_1, u_1} Y'
hY' : Function.Bijective (α := RightHomotopyClass X Y') (rightHomotopyClassToHom L)
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
have inr : ∀ (hY' : Function.Bijective (α := LeftHomotopyClass X Y') (leftHomotopyClassToHom L)),
  Function.Bijective (α := LeftHomotopyClass X Y) (leftHomotopyClassToHom L)
Tactic: simp only [← bijective_leftHomotopyClassToHom_iff_bijective_rightHomotopyClassToHom] at hY' ⊢
Cleared hypotheses: hY'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y : C
inst_4 : IsCofibrant.{v_1, u_1} X
inst_5 : IsFibrant.{v_1, u_1} Y
this :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h : ¬IsCofibrant.{v_1, u_1} Y
Y' : C
w : IsCofibrant.{v_1, u_1} Y'
p : Y' ⟶ Y
left : Fibration p
right : WeakEquivalence p
h_1 : IsFibrant.{v_1, u_1} Y'
hY' : Function.Bijective (α := LeftHomotopyClass X Y') (leftHomotopyClassToHom L)
⊢ Function.Bijective (α := LeftHomotopyClass X Y) (leftHomotopyClassToHom L)
have this₁ : IsIso (L.map p)
Tactic: have := Localization.inverts L (weakEquivalences _) p
      (by rwa [← weakEquivalence_iff])
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y : C
inst_4 : IsCofibrant.{v_1, u_1} X
inst_5 : IsFibrant.{v_1, u_1} Y
this_1 :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h : ¬IsCofibrant.{v_1, u_1} Y
Y' : C
w : IsCofibrant.{v_1, u_1} Y'
p : Y' ⟶ Y
left : Fibration p
right : WeakEquivalence p
h_1 : IsFibrant.{v_1, u_1} Y'
hY' : Function.Bijective (α := LeftHomotopyClass X Y') (leftHomotopyClassToHom L)
this : IsIso (L.map p)
⊢ Function.Bijective (α := LeftHomotopyClass X Y) (leftHomotopyClassToHom L)
have inr : Function.Bijective (α := LeftHomotopyClass X Y') (β := L.obj X ⟶ L.obj Y)
  (Function.comp (β := LeftHomotopyClass X Y) (leftHomotopyClassToHom L) fun (f : LeftHomotopyClass X Y') ↦
    f.postcomp p)
Tactic: rw [← Function.Bijective.of_comp_iff _
      (LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence _ p)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y : C
inst_4 : IsCofibrant.{v_1, u_1} X
inst_5 : IsFibrant.{v_1, u_1} Y
this_1 :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h : ¬IsCofibrant.{v_1, u_1} Y
Y' : C
w : IsCofibrant.{v_1, u_1} Y'
p : Y' ⟶ Y
left : Fibration p
right : WeakEquivalence p
h_1 : IsFibrant.{v_1, u_1} Y'
hY' : Function.Bijective (α := LeftHomotopyClass X Y') (leftHomotopyClassToHom L)
this : IsIso (L.map p)
⊢ Function.Bijective (α := LeftHomotopyClass X Y') (β := L.obj X ⟶ L.obj Y)
    (Function.comp (β := LeftHomotopyClass X Y) (leftHomotopyClassToHom L) fun (f : LeftHomotopyClass X Y') ↦
      f.postcomp p)
have h : Eq (α := LeftHomotopyClass X Y' → (L.obj X ⟶ L.obj Y))
  (Function.comp (β := LeftHomotopyClass X Y) (leftHomotopyClassToHom L) fun (f : LeftHomotopyClass X Y') ↦
    f.postcomp p)
  ((⇑(Iso.homCongr (Iso.refl (L.obj X)) (asIso (L.map p))) : (a : L.obj X ⟶ L.obj Y') → L.obj X ⟶ L.obj Y) ∘
    leftHomotopyClassToHom L)
Tactic: convert! (Iso.homCongr (Iso.refl (L.obj X)) (asIso (L.map p))).bijective.comp hY'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y : C
inst_4 : IsCofibrant.{v_1, u_1} X
inst_5 : IsFibrant.{v_1, u_1} Y
this_1 :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h : ¬IsCofibrant.{v_1, u_1} Y
Y' : C
w : IsCofibrant.{v_1, u_1} Y'
p : Y' ⟶ Y
left : Fibration p
right : WeakEquivalence p
h_1 : IsFibrant.{v_1, u_1} Y'
hY' : Function.Bijective (α := LeftHomotopyClass X Y') (leftHomotopyClassToHom L)
this : IsIso (L.map p)
⊢ Eq (α := LeftHomotopyClass X Y' → (L.obj X ⟶ L.obj Y))
    (Function.comp (β := LeftHomotopyClass X Y) (leftHomotopyClassToHom L) fun (f : LeftHomotopyClass X Y') ↦
      f.postcomp p)
    ((⇑(Iso.homCongr (Iso.refl (L.obj X)) (asIso (L.map p))) : (a : L.obj X ⟶ L.obj Y') → L.obj X ⟶ L.obj Y) ∘
      leftHomotopyClassToHom L)
have h : ∀ (f : LeftHomotopyClass X Y'),
  Eq (α := L.obj X ⟶ L.obj Y)
    (Function.comp (β := LeftHomotopyClass X Y) (leftHomotopyClassToHom L)
      (fun (f : LeftHomotopyClass X Y') ↦ f.postcomp p) f)
    (((⇑(Iso.homCongr (Iso.refl (L.obj X)) (asIso (L.map p))) : (a : L.obj X ⟶ L.obj Y') → L.obj X ⟶ L.obj Y) ∘
        leftHomotopyClassToHom L)
      f)
Tactic: ext f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y : C
inst_4 : IsCofibrant.{v_1, u_1} X
inst_5 : IsFibrant.{v_1, u_1} Y
this_1 :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h : ¬IsCofibrant.{v_1, u_1} Y
Y' : C
w : IsCofibrant.{v_1, u_1} Y'
p : Y' ⟶ Y
left : Fibration p
right : WeakEquivalence p
h_1 : IsFibrant.{v_1, u_1} Y'
hY' : Function.Bijective (α := LeftHomotopyClass X Y') (leftHomotopyClassToHom L)
this : IsIso (L.map p)
f : LeftHomotopyClass X Y'
⊢ Eq (α := L.obj X ⟶ L.obj Y)
    (Function.comp (β := LeftHomotopyClass X Y) (leftHomotopyClassToHom L)
      (fun (f : LeftHomotopyClass X Y') ↦ f.postcomp p) f)
    (((⇑(Iso.homCongr (Iso.refl (L.obj X)) (asIso (L.map p))) : (a : L.obj X ⟶ L.obj Y') → L.obj X ⟶ L.obj Y) ∘
        leftHomotopyClassToHom L)
      f)
have h : ∀ (f : X ⟶ Y'),
  Eq (α := L.obj X ⟶ L.obj Y)
    (Function.comp (β := LeftHomotopyClass X Y) (leftHomotopyClassToHom L)
      (fun (f : LeftHomotopyClass X Y') ↦ f.postcomp p) (LeftHomotopyClass.mk f))
    (Function.comp (α := LeftHomotopyClass X Y')
      (⇑(Iso.homCongr (Iso.refl (L.obj X)) (asIso (L.map p))) : (a : L.obj X ⟶ L.obj Y') → L.obj X ⟶ L.obj Y)
      (leftHomotopyClassToHom L) (LeftHomotopyClass.mk f))
Tactic: obtain ⟨f, rfl⟩ := f.mk_surjective
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
have inr : ∀
  (this :
    ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
      Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)),
  ¬IsFibrant.{v_1, u_1} X → Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
Tactic: wlog _ : IsFibrant X generalizing X
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
inr :
  ∀
    (this :
      ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
        Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)),
    ¬IsFibrant.{v_1, u_1} X → Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
have wlog : ∀ (X : C) [IsCofibrant.{v_1, u_1} X],
  IsFibrant.{v_1, u_1} X → Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
Tactic: wlog _ : IsFibrant X generalizing X
Cleared hypotheses: inst_4
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
this :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_1 : ¬IsFibrant.{v_1, u_1} X
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
have inr : ∀ (X' : C) (i : X ⟶ X'),
  Cofibration i →
    WeakEquivalence i →
      IsFibrant.{v_1, u_1} X' → Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
Tactic: obtain ⟨X', i, _, _, _⟩ : ∃ (X' : C) (i : X ⟶ X'), Cofibration i ∧ WeakEquivalence i ∧
        IsFibrant X' :=
      ⟨_, FibrantObject.HoCat.iResolutionObj X, inferInstance, inferInstance, inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
this :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_1 : ¬IsFibrant.{v_1, u_1} X
X' : C
i : X ⟶ X'
left : Cofibration i
left_1 : WeakEquivalence i
right : IsFibrant.{v_1, u_1} X'
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
have x : IsCofibrant.{v_1, u_1} X'
Tactic: have _ := isCofibrant_of_cofibration i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
this :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_1 : ¬IsFibrant.{v_1, u_1} X
X' : C
i : X ⟶ X'
left : Cofibration i
left_1 : WeakEquivalence i
right : IsFibrant.{v_1, u_1} X'
h_2 : IsCofibrant.{v_1, u_1} X'
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
have hX' : Function.Bijective (α := RightHomotopyClass X' Y) (rightHomotopyClassToHom L)
Tactic: have hX' := this X' inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
this :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_1 : ¬IsFibrant.{v_1, u_1} X
X' : C
i : X ⟶ X'
left : Cofibration i
left_1 : WeakEquivalence i
right : IsFibrant.{v_1, u_1} X'
h_2 : IsCofibrant.{v_1, u_1} X'
hX' : Function.Bijective (α := RightHomotopyClass X' Y) (rightHomotopyClassToHom L)
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
have this₁ : IsIso (L.map i)
Tactic: have := Localization.inverts L (weakEquivalences _) i
      (by rwa [← weakEquivalence_iff])
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
this_1 :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_1 : ¬IsFibrant.{v_1, u_1} X
X' : C
i : X ⟶ X'
left : Cofibration i
left_1 : WeakEquivalence i
right : IsFibrant.{v_1, u_1} X'
h_2 : IsCofibrant.{v_1, u_1} X'
hX' : Function.Bijective (α := RightHomotopyClass X' Y) (rightHomotopyClassToHom L)
this : IsIso (L.map i)
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
have inr : Function.Bijective (α := RightHomotopyClass X' Y) (β := L.obj X ⟶ L.obj Y)
  (Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L) fun (g : RightHomotopyClass X' Y) ↦
    g.precomp i)
Tactic: rw [← Function.Bijective.of_comp_iff _
      (RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence Y i)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
this_1 :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_1 : ¬IsFibrant.{v_1, u_1} X
X' : C
i : X ⟶ X'
left : Cofibration i
left_1 : WeakEquivalence i
right : IsFibrant.{v_1, u_1} X'
h_2 : IsCofibrant.{v_1, u_1} X'
hX' : Function.Bijective (α := RightHomotopyClass X' Y) (rightHomotopyClassToHom L)
this : IsIso (L.map i)
⊢ Function.Bijective (α := RightHomotopyClass X' Y) (β := L.obj X ⟶ L.obj Y)
    (Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L) fun (g : RightHomotopyClass X' Y) ↦
      g.precomp i)
have h : Eq (α := RightHomotopyClass X' Y → (L.obj X ⟶ L.obj Y))
  (Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L) fun (g : RightHomotopyClass X' Y) ↦
    g.precomp i)
  ((⇑((asIso (L.map i)).homCongr (Iso.refl (L.obj Y))).symm : (a : L.obj X' ⟶ L.obj Y) → L.obj X ⟶ L.obj Y) ∘
    rightHomotopyClassToHom L)
Tactic: convert! (Iso.homCongr (asIso (L.map i)) (Iso.refl (L.obj Y))).symm.bijective.comp hX'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
this_1 :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_1 : ¬IsFibrant.{v_1, u_1} X
X' : C
i : X ⟶ X'
left : Cofibration i
left_1 : WeakEquivalence i
right : IsFibrant.{v_1, u_1} X'
h_2 : IsCofibrant.{v_1, u_1} X'
hX' : Function.Bijective (α := RightHomotopyClass X' Y) (rightHomotopyClassToHom L)
this : IsIso (L.map i)
⊢ Eq (α := RightHomotopyClass X' Y → (L.obj X ⟶ L.obj Y))
    (Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L) fun (g : RightHomotopyClass X' Y) ↦
      g.precomp i)
    ((⇑((asIso (L.map i)).homCongr (Iso.refl (L.obj Y))).symm : (a : L.obj X' ⟶ L.obj Y) → L.obj X ⟶ L.obj Y) ∘
      rightHomotopyClassToHom L)
have h : ∀ (f : RightHomotopyClass X' Y),
  Eq (α := L.obj X ⟶ L.obj Y)
    (Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
      (fun (g : RightHomotopyClass X' Y) ↦ g.precomp i) f)
    (((⇑((asIso (L.map i)).homCongr (Iso.refl (L.obj Y))).symm : (a : L.obj X' ⟶ L.obj Y) → L.obj X ⟶ L.obj Y) ∘
        rightHomotopyClassToHom L)
      f)
Tactic: ext f