awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
E₁ : Type u_3
E₂ : Type u_4
inst_2 : Category.{v_3, u_3} E₁
inst_3 : Category.{v_4, u_4} E₂
F₁ : Functor.{v_1, v_3, u_1, u_3} C₁ E₁
F₂ : Functor.{v_2, v_4, u_2, u_4} C₂ E₂
h₁ : W₁.IsInvertedBy F₁
h₂ : W₂.IsInvertedBy F₂
x x_1 : C₁ × C₂
f : x ⟶ x_1
hf : W₁.prod W₂ f
⊢ IsIso ((F₁.prod F₂).map f)
have rw : IsIso ((F₁.prod F₂).map f).1 ∧ IsIso ((F₁.prod F₂).map f).2
Tactic: rw [isIso_prod_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (goal)
Goal:
J : Type w
C : J → Type u
D : J → Type u'
inst : (j : J) → Category.{v, u} (C j)
inst_1 : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty.{v, u} (C j)
F : (j : J) → Functor.{v, v', u, u'} (C j) (D j)
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X Y : (j : J) → C j
f : X ⟶ Y
hf : MorphismProperty.pi (C := C) W f
⊢ IsIso ((Functor.pi (C := C) (D := D) F).map f)
have rw : ∀ (i : J), IsIso ((Functor.pi (C := C) (D := D) F).map f i)
Tactic: rw [isIso_pi_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F₁ F₂ : FunctorsInverting.{v, u, v', u'} W D
h :
  F₁.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) =
    F₂.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
⊢ F₁ = F₂
have mk : ∀ (obj : Functor.{v, v', u, u'} C D) (property : W.IsInvertedBy obj)
  (h :
    ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
        (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj
          property) =
      F₂.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)),
  ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj property = F₂
Tactic: cases F₁
Cleared hypotheses: F₁, h
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F₂ : FunctorsInverting.{v, u, v', u'} W D
obj : Functor.{v, v', u, u'} C D
property : W.IsInvertedBy obj
h :
  ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
      (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj property) =
    F₂.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
⊢ ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj property = F₂
have mk : ∀ (obj_1 : Functor.{v, v', u, u'} C D) (property_1 : W.IsInvertedBy obj_1)
  (h :
    ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
        (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj
          property) =
      ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
        (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj_1
          property_1)),
  Eq (α := FunctorsInverting.{v, u, v', u'} W D)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj property)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj_1 property_1)
Tactic: cases F₂
Cleared hypotheses: F₂, h
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
obj : Functor.{v, v', u, u'} C D
property : W.IsInvertedBy obj
obj_1 : Functor.{v, v', u, u'} C D
property_1 : W.IsInvertedBy obj_1
h :
  ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
      (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj property) =
    ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
      (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj_1
        property_1)
⊢ Eq (α := FunctorsInverting.{v, u, v', u'} W D)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj property)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj_1 property_1)
have mk : ∀
  (property_2 :
    W.IsInvertedBy
      (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
        (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj
          property))),
  Eq (α := FunctorsInverting.{v, u, v', u'} W D)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj property)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
      (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F)
        (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{v, v', u, u'} C D) ↦ W.IsInvertedBy F) obj property))
      property_2)
Tactic: subst h
Cleared hypotheses: obj_1, property_1, h
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
⊢ W.isoClosure.IsInvertedBy F ↔ W.IsInvertedBy F
have mp : W.isoClosure.IsInvertedBy F → W.IsInvertedBy F
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
mp : W.isoClosure.IsInvertedBy F → W.IsInvertedBy F
⊢ W.isoClosure.IsInvertedBy F ↔ W.IsInvertedBy F
have mpr : W.IsInvertedBy F → W.isoClosure.IsInvertedBy F
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
h : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
⊢ W.isoClosure f → IsIso (F.map f)
have mpr : ∀ (X' Y' : C) (f' : X' ⟶ Y') (hf' : W f') (e : Arrow.mk f' ≅ Arrow.mk f), IsIso (F.map f)
Tactic: ⟨X', Y', f', hf', ⟨e⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
h : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : W f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ IsIso (F.map f)
have mpr : IsIso (F.map (Arrow.Hom.left e.inv) ≫ F.map f' ≫ F.map (Arrow.Hom.right e.hom))
Tactic: simp only [Arrow.iso_w' e, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
h : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : W f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ IsIso (F.map (Arrow.Hom.left e.inv) ≫ F.map f' ≫ F.map (Arrow.Hom.right e.hom))
have this : IsIso (F.map f')
Tactic: have := h _ hf'
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
W : MorphismProperty.{v_1, u_1} C₁
F : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
G : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
inst_3 : G.ReflectsIsomorphisms
⊢ W.IsInvertedBy (F ⋙ G) ↔ W.IsInvertedBy F
have mp : W.IsInvertedBy (F ⋙ G) → W.IsInvertedBy F
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
W : MorphismProperty.{v_1, u_1} C₁
F : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
G : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
inst_3 : G.ReflectsIsomorphisms
mp : W.IsInvertedBy (F ⋙ G) → W.IsInvertedBy F
⊢ W.IsInvertedBy (F ⋙ G) ↔ W.IsInvertedBy F
have mpr : W.IsInvertedBy F → W.IsInvertedBy (F ⋙ G)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (hypothesis)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
W : MorphismProperty.{v_1, u_1} C₁
F : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
G : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
inst_3 : G.ReflectsIsomorphisms
h : W.IsInvertedBy (F ⋙ G)
X Y : C₁
f : X ⟶ Y
hf : W f
⊢ IsIso (F.map f)
have this : IsIso (G.map (F.map f))
Tactic: have : IsIso (G.map (F.map f)) := h _ hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
⊢ W.IsInvertedBy F ↔ W.map F ≤ isomorphisms D
have rw : W ≤ inverseImage (isomorphisms D) F ↔ W.map F ≤ isomorphisms D
Tactic: rw [iff_le_inverseImage_isomorphisms, map_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
rw : W ≤ inverseImage (isomorphisms D) F ↔ W.map F ≤ isomorphisms D
⊢ W.IsInvertedBy F ↔ W.map F ≤ isomorphisms D
have rw₁ : W ≤ inverseImage (isomorphisms D) F ↔ W ≤ inverseImage (isomorphisms D) F
Tactic: rw [iff_le_inverseImage_isomorphisms, map_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
X Y Z : C
i : X ⟶ Y
j : Y ⟶ Z
hi : T.llp i
hj : T.llp j
x x_1 : C
p : x ⟶ x_1
hp : T p
⊢ HasLiftingProperty (i ≫ j) p
have this : HasLiftingProperty i p
Tactic: have := hi _ hp
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
X Y Z : C
i : X ⟶ Y
j : Y ⟶ Z
hi : T.llp i
hj : T.llp j
x x_1 : C
p : x ⟶ x_1
hp : T p
this : HasLiftingProperty i p
⊢ HasLiftingProperty (i ≫ j) p
have this₁ : HasLiftingProperty j p
Tactic: have := hj _ hp
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
X Y Z : C
i : X ⟶ Y
j : Y ⟶ Z
hi : T.rlp i
hj : T.rlp j
x x_1 : C
p : x ⟶ x_1
hp : T p
⊢ HasLiftingProperty p (i ≫ j)
have this : HasLiftingProperty p i
Tactic: have := hi _ hp
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
X Y Z : C
i : X ⟶ Y
j : Y ⟶ Z
hi : T.rlp i
hj : T.rlp j
x x_1 : C
p : x ⟶ x_1
hp : T p
this : HasLiftingProperty p i
⊢ HasLiftingProperty p (i ≫ j)
have this₁ : HasLiftingProperty p j
Tactic: have := hj _ hp
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
J : Type u_1
⊢ T.llp.IsStableUnderCoproductsOfShape J
have hW : ∀ (X₁ X₂ : J → C) [inst_1 : Limits.HasCoproduct.{u_1, v, u} X₁] [inst_2 : Limits.HasCoproduct.{u_1, v, u} X₂]
  (f : (j : J) → X₁ j ⟶ X₂ j),
  (∀ (j : J), T.llp (f j)) →
    T.llp (X := Limits.sigmaObj.{u_1, v, u} X₁) (Y := Limits.sigmaObj.{u_1, v, u} X₂) (Limits.Sigma.map f)
Tactic: apply IsStableUnderCoproductsOfShape.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
J : Type u_1
A B : J → C
inst_1 : Limits.HasCoproduct.{u_1, v, u} A
inst_2 : Limits.HasCoproduct.{u_1, v, u} B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.llp (f j)
X Y : C
p : X ⟶ Y
hp : T p
⊢ HasLiftingProperty (A := Limits.sigmaObj.{u_1, v, u} A) (B := Limits.sigmaObj.{u_1, v, u} B) (Limits.Sigma.map f) p
have this : ∀ (j : J), HasLiftingProperty (f j) p
Tactic: have := fun j ↦ hf j _ hp
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
J : Type u_1
⊢ T.rlp.IsStableUnderProductsOfShape J
have hW : ∀ (X₁ X₂ : J → C) [inst_1 : Limits.HasProduct.{u_1, v, u} X₁] [inst_2 : Limits.HasProduct.{u_1, v, u} X₂]
  (f : (j : J) → X₁ j ⟶ X₂ j),
  (∀ (j : J), T.rlp (f j)) →
    T.rlp (X := Limits.piObj.{u_1, v, u} X₁) (Y := Limits.piObj.{u_1, v, u} X₂) (Limits.Pi.map f)
Tactic: apply IsStableUnderProductsOfShape.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
J : Type u_1
A B : J → C
inst_1 : Limits.HasProduct.{u_1, v, u} A
inst_2 : Limits.HasProduct.{u_1, v, u} B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.rlp (f j)
X Y : C
p : X ⟶ Y
hp : T p
⊢ HasLiftingProperty (X := Limits.piObj.{u_1, v, u} A) (Y := Limits.piObj.{u_1, v, u} B) p (Limits.Pi.map f)
have this : ∀ (j : J), HasLiftingProperty p (f j)
Tactic: have := fun j ↦ hf j _ hp
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ T ≤ T.rlp.llp
have rw : T.rlp ≤ T.rlp
Tactic: rw [le_llp_iff_le_rlp]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ T.pushouts.rlp = T.rlp
have a : T.pushouts.rlp ≤ T.rlp
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
a : T.pushouts.rlp ≤ T.rlp
⊢ T.pushouts.rlp = T.rlp
have a₁ : T.rlp ≤ T.pushouts.rlp
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ T.rlp ≤ T.pushouts.rlp
have a : T.pushouts ≤ T.rlp.llp
Tactic: rw [← le_llp_iff_le_rlp]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
A B : C
i : A ⟶ B
hi : coproducts.{w, v, u} T i
⊢ T.rlp.llp i
have hi₁ : ∃ (J : Type w), colimitsOfShape.{v, u, w, w} T (Discrete J) i
Tactic: rw [coproducts_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
A B : C
i : A ⟶ B
hi : ∃ (J : Type w), colimitsOfShape.{v, u, w, w} T (Discrete J) i
⊢ T.rlp.llp i
have obtain : ∀ (J : Type w) (hi : colimitsOfShape.{v, u, w, w} T (Discrete J) i), T.rlp.llp i
Tactic: obtain ⟨J, hi⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ (coproducts.{w, v, u} T).rlp = T.rlp
have a : (coproducts.{w, v, u} T).rlp ≤ T.rlp
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
a : (coproducts.{w, v, u} T).rlp ≤ T.rlp
⊢ (coproducts.{w, v, u} T).rlp = T.rlp
have a₁ : T.rlp ≤ (coproducts.{w, v, u} T).rlp
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ T.rlp ≤ (coproducts.{w, v, u} T).rlp
have a : coproducts.{w, v, u} T ≤ T.rlp.llp
Tactic: rw [← le_llp_iff_le_rlp]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ T.retracts.rlp = T.rlp
have a : T.retracts.rlp ≤ T.rlp
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
a : T.retracts.rlp ≤ T.rlp
⊢ T.retracts.rlp = T.rlp
have a₁ : T.rlp ≤ T.retracts.rlp
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ T.rlp ≤ T.retracts.rlp
have a : T.retracts ≤ T.rlp.llp
Tactic: rw [← le_llp_iff_le_rlp]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
G : Functor.{v, v_1, u, u_1} C D
inst_2 : G.IsEquivalence
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty (G.map i) (G.map p) ↔ HasLiftingProperty i p
have simp : MorphismProperty.rlp (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ A) (Y := fun (x : Unit) ↦ B) fun (x : Unit) ↦ i)
    (G.asEquivalence.inverse.map (G.map p)) ↔
  MorphismProperty.rlp (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ A) (Y := fun (x : Unit) ↦ B) fun (x : Unit) ↦ i)
    p
Tactic: simp only [dsimp% G.asEquivalence.toAdjunction.hasLiftingProperty_iff,
    ← MorphismProperty.rlp_ofHoms_iff_hasLiftingProperty Unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.InducedShiftSequence (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_3, u_2, u_3} D A
G : Functor.{v_1, v_3, u_1, u_3} C A
e : L ⋙ F ≅ G
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : G.ShiftSequence M
F' : M → Functor.{v_2, v_3, u_2, u_3} D A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst_6 : Full (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_7 : Faithful (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_8 : HasShift.{v_2, u_2, u_4} D M
inst_9 : L.CommShift M
a : M
⊢ Eq (α := shiftFunctor.{v_2, u_2, u_4} D (A := M) 0 ⋙ F' a ≅ F' a) (induced.shiftIso L G M F' e' 0 a a ⋯)
    (isoWhiskerRight (shiftFunctorZero D M) (F' a) ≪≫ (F' a).leftUnitor)
have w : Eq (α := shiftFunctor.{v_2, u_2, u_4} D (A := M) 0 ⋙ F' a ⟶ F' a) (Iso.hom (induced.shiftIso L G M F' e' 0 a a sorry))
  (Iso.hom (isoWhiskerRight (shiftFunctorZero D M) (F' a) ≪≫ (F' a).leftUnitor))
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.InducedShiftSequence (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_3, u_2, u_3} D A
G : Functor.{v_1, v_3, u_1, u_3} C A
e : L ⋙ F ≅ G
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : G.ShiftSequence M
F' : M → Functor.{v_2, v_3, u_2, u_3} D A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst_6 : Full (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_7 : Faithful (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_8 : HasShift.{v_2, u_2, u_4} D M
inst_9 : L.CommShift M
a : M
⊢ Eq (α := shiftFunctor.{v_2, u_2, u_4} D (A := M) 0 ⋙ F' a ⟶ F' a) (Iso.hom (induced.shiftIso L G M F' e' 0 a a ⋯))
    (Iso.hom (isoWhiskerRight (shiftFunctorZero D M) (F' a) ≪≫ (F' a).leftUnitor))
have w : Eq (α :=
  obj (obj (whiskeringLeft C D A) L) (shiftFunctor.{v_2, u_2, u_4} D (A := M) 0 ⋙ F' a) ⟶
    obj (obj (whiskeringLeft C D A) L) (F' a))
  (map (obj (whiskeringLeft C D A) L) (Iso.hom (induced.shiftIso L G M F' e' 0 a a sorry)))
  (map (obj (whiskeringLeft C D A) L) (Iso.hom (isoWhiskerRight (shiftFunctorZero D M) (F' a) ≪≫ (F' a).leftUnitor)))
Tactic: apply ((whiskeringLeft C D A).obj L).map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.InducedShiftSequence (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_3, u_2, u_3} D A
G : Functor.{v_1, v_3, u_1, u_3} C A
e : L ⋙ F ≅ G
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : G.ShiftSequence M
F' : M → Functor.{v_2, v_3, u_2, u_3} D A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst_6 : Full (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_7 : Faithful (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_8 : HasShift.{v_2, u_2, u_4} D M
inst_9 : L.CommShift M
a : M
⊢ Eq (α :=
    obj (obj (whiskeringLeft C D A) L) (shiftFunctor.{v_2, u_2, u_4} D (A := M) 0 ⋙ F' a) ⟶
      obj (obj (whiskeringLeft C D A) L) (F' a))
    (map (obj (whiskeringLeft C D A) L) (Iso.hom (induced.shiftIso L G M F' e' 0 a a ⋯)))
    (map (obj (whiskeringLeft C D A) L) (Iso.hom (isoWhiskerRight (shiftFunctorZero D M) (F' a) ≪≫ (F' a).leftUnitor)))
have w : ∀ (K : C),
  Eq (α :=
    (obj (obj (whiskeringLeft C D A) L) (shiftFunctor.{v_2, u_2, u_4} D (A := M) 0 ⋙ F' a)).obj K ⟶
      (obj (obj (whiskeringLeft C D A) L) (F' a)).obj K)
    (NatTrans.app (map (obj (whiskeringLeft C D A) L) (Iso.hom (induced.shiftIso L G M F' e' 0 a a sorry))) K)
    (NatTrans.app
      (map (obj (whiskeringLeft C D A) L)
        (Iso.hom (isoWhiskerRight (shiftFunctorZero D M) (F' a) ≪≫ (F' a).leftUnitor)))
      K)
Tactic: ext K
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.InducedShiftSequence (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_3, u_2, u_3} D A
G : Functor.{v_1, v_3, u_1, u_3} C A
e : L ⋙ F ≅ G
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : G.ShiftSequence M
F' : M → Functor.{v_2, v_3, u_2, u_3} D A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst_6 : Full (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_7 : Faithful (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_8 : HasShift.{v_2, u_2, u_4} D M
inst_9 : L.CommShift M
a : M
K : C
⊢ Eq (α :=
    (obj (obj (whiskeringLeft C D A) L) (shiftFunctor.{v_2, u_2, u_4} D (A := M) 0 ⋙ F' a)).obj K ⟶
      (obj (obj (whiskeringLeft C D A) L) (F' a)).obj K)
    (NatTrans.app (map (obj (whiskeringLeft C D A) L) (Iso.hom (induced.shiftIso L G M F' e' 0 a a ⋯))) K)
    (NatTrans.app
      (map (obj (whiskeringLeft C D A) L)
        (Iso.hom (isoWhiskerRight (shiftFunctorZero D M) (F' a) ≪≫ (F' a).leftUnitor)))
      K)
have w : Eq (α :=
  (F' a).obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_4} D (A := M) 0) (L.obj K)) ⟶ (F' a).obj (L.obj K))
  (NatTrans.app (Iso.hom (induced.shiftIso L G M F' e' 0 a a sorry)) (L.obj K))
  ((F' a).map (NatTrans.app (Iso.hom (shiftFunctorZero D M)) (L.obj K)) ≫ 𝟙 ((F' a).obj (L.obj K)))
Tactic: dsimp