awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
X Y : D
f_1 : X ⟶ Y
h : (W.strictMap F).isoClosure f_1
w w_1 : D
f : w ⟶ w_1
hf : W.strictMap F f
hf' : Nonempty.{v_1 + 1} (Arrow.mk f ≅ Arrow.mk f_1)
⊢ W.map F f_1
have h : ∀ ⦃X_1 Y_1 : D⦄ {X_2 Y_2 : C} {f : X_2 ⟶ Y_2} (hf : W f) (hf' : Nonempty.{v_1 + 1} (Arrow.mk (F.map f) ≅ Arrow.mk f_1)),
  W.map F f_1
Tactic: obtain ⟨hf⟩ := hf
Cleared hypotheses: w, w_1, f, hf, hf'
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
⊢ (P.map F).RespectsIso
have rw : (P.strictMap F).isoClosure.RespectsIso
Tactic: rw [map_eq_isoClosure]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
Q : MorphismProperty.{v_1, u_1} D
inst_2 : Q.RespectsIso
⊢ P.map F ≤ Q ↔ P ≤ Q.inverseImage F
have rw : (P.strictMap F).isoClosure ≤ Q ↔ P ≤ Q.inverseImage F
Tactic: rw [map_eq_isoClosure, isoClosure_le_iff, strictMap_le_iff_le_inverseImage]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
Q : MorphismProperty.{v_1, u_1} D
inst_2 : Q.RespectsIso
rw : (P.strictMap F).isoClosure ≤ Q ↔ P ≤ Q.inverseImage F
⊢ P.map F ≤ Q ↔ P ≤ Q.inverseImage F
have rw₁ : P.strictMap F ≤ Q ↔ P ≤ Q.inverseImage F
Tactic: rw [map_eq_isoClosure, isoClosure_le_iff, strictMap_le_iff_le_inverseImage]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
Q : MorphismProperty.{v_1, u_1} D
inst_2 : Q.RespectsIso
rw : (P.strictMap F).isoClosure ≤ Q ↔ P ≤ Q.inverseImage F
rw₁ : P.strictMap F ≤ Q ↔ P ≤ Q.inverseImage F
⊢ P.map F ≤ Q ↔ P ≤ Q.inverseImage F
have rw₂ : P ≤ Q.inverseImage F ↔ P ≤ Q.inverseImage F
Tactic: rw [map_eq_isoClosure, isoClosure_le_iff, strictMap_le_iff_le_inverseImage]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
⊢ P.isoClosure.map F = P.map F
have a : P.isoClosure.map F ≤ P.map F
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
a : P.isoClosure.map F ≤ P.map F
⊢ P.isoClosure.map F = P.map F
have a₁ : P.map F ≤ P.isoClosure.map F
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
⊢ P.isoClosure.map F ≤ P.map F
have a : P.isoClosure.strictMap F ≤ (P.strictMap F).isoClosure
Tactic: rw [map_eq_isoClosure, map_eq_isoClosure, isoClosure_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
⊢ P.map (𝟭 C) = P
have rw : P.isoClosure = P
Tactic: rw [map_id_eq_isoClosure, P.isoClosure_eq_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
rw : P.isoClosure = P
⊢ P.map (𝟭 C) = P
have rw₁ : P = P
Tactic: rw [map_id_eq_isoClosure, P.isoClosure_eq_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
G : Functor.{v_1, v_2, u_1, u_2} D E
⊢ (P.map F).map G = P.map (F ⋙ G)
have a : (P.map F).map G ≤ P.map (F ⋙ G)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
G : Functor.{v_1, v_2, u_1, u_2} D E
a : (P.map F).map G ≤ P.map (F ⋙ G)
⊢ (P.map F).map G = P.map (F ⋙ G)
have a₁ : P.map (F ⋙ G) ≤ (P.map F).map G
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
G : Functor.{v_1, v_2, u_1, u_2} D E
⊢ (P.map F).map G ≤ P.map (F ⋙ G)
have a : P.map F ≤ (P.map (F ⋙ G)).inverseImage G
Tactic: rw [map_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
G : Functor.{v_1, v_2, u_1, u_2} D E
X Y : D
f : X ⟶ Y
⊢ P.map F f → (P.map (F ⋙ G)).inverseImage G f
have a : ∀ (X' Y' : C) (f' : X' ⟶ Y') (hf' : P f') (e : Arrow.mk (F.map f') ≅ Arrow.mk f), (P.map (F ⋙ G)).inverseImage G f
Tactic: ⟨X', Y', f', hf', ⟨e⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
G : Functor.{v_1, v_2, u_1, u_2} D E
⊢ P.map (F ⋙ G) ≤ (P.map F).map G
have a : P ≤ ((P.map F).map G).inverseImage (F ⋙ G)
Tactic: rw [map_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
F G : Functor.{v, v_1, u, u_1} C D
e : F ≅ G
⊢ P.map F = P.map G
have revert : ∀ {F G : Functor.{v, v_1, u, u_1} C D} (e : F ≅ G), P.map F = P.map G
Tactic: revert F G e
Cleared hypotheses: F, G, e
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
⊢ ∀ {F G : Functor.{v, v_1, u, u_1} C D} (e : F ≅ G), P.map F = P.map G
have suffices : ∀ {F G : Functor.{v, v_1, u, u_1} C D} (x : F ≅ G), P.map F ≤ P.map G
Tactic: suffices ∀ {F G : C ⥤ D} (_ : F ≅ G), P.map F ≤ P.map G from
    fun F G e => le_antisymm (this e) (this e.symm)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
F G : Functor.{v, v_1, u, u_1} C D
e : F ≅ G
X Y : D
f : X ⟶ Y
⊢ P.map F f → P.map G f
have this : ∀ (X' Y' : C) (f' : X' ⟶ Y') (hf' : P f') (e' : Arrow.mk (F.map f') ≅ Arrow.mk f), P.map G f
Tactic: ⟨X', Y', f', hf', ⟨e'⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v_1, u_1} D
inst_2 : P.RespectsIso
E : Equivalence.{v, v_1, u, u_1} C D
⊢ P.inverseImage E.functor = P.map E.inverse
have a : P.inverseImage E.functor ≤ P.map E.inverse
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v_1, u_1} D
inst_2 : P.RespectsIso
E : Equivalence.{v, v_1, u, u_1} C D
a : P.inverseImage E.functor ≤ P.map E.inverse
⊢ P.inverseImage E.functor = P.map E.inverse
have a₁ : P.map E.inverse ≤ P.inverseImage E.functor
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v_1, u_1} D
inst_2 : P.RespectsIso
E : Equivalence.{v, v_1, u, u_1} C D
X Y : C
f : X ⟶ Y
hf : P.inverseImage E.functor f
⊢ P.map E.inverse f
have a : Arrow.mk (E.inverse.map (E.functor.map f)) ≅ Arrow.mk f
Tactic: refine ⟨_, _, _, hf, ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v_1, u_1} D
inst_2 : P.RespectsIso
E : Equivalence.{v, v_1, u, u_1} C D
⊢ P.map E.inverse ≤ P.inverseImage E.functor
have a : P ≤ (P.inverseImage E.functor).inverseImage E.inverse
Tactic: rw [map_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v_1, u_1} D
inst_2 : P.RespectsIso
F : Functor.{v, v_1, u, u_1} C D
inst_3 : F.IsEquivalence
⊢ (P.inverseImage F).map F = P
have erw : (P.map F.asEquivalence.inverse).map F = P
Tactic: erw [P.inverseImage_equivalence_inverse_eq_map_functor F.asEquivalence, map_map,
    P.map_eq_of_iso F.asEquivalence.counitIso, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v_1, u_1} D
inst_2 : P.RespectsIso
F : Functor.{v, v_1, u, u_1} C D
inst_3 : F.IsEquivalence
erw : (P.map F.asEquivalence.inverse).map F = P
⊢ (P.inverseImage F).map F = P
have erw₁ : P.map (F.asEquivalence.inverse ⋙ F) = P
Tactic: erw [P.inverseImage_equivalence_inverse_eq_map_functor F.asEquivalence, map_map,
    P.map_eq_of_iso F.asEquivalence.counitIso, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v_1, u_1} D
inst_2 : P.RespectsIso
F : Functor.{v, v_1, u, u_1} C D
inst_3 : F.IsEquivalence
erw : (P.map F.asEquivalence.inverse).map F = P
erw₁ : P.map (F.asEquivalence.inverse ⋙ F) = P
⊢ (P.inverseImage F).map F = P
have erw₂ : P.map (𝟭 D) = P
Tactic: erw [P.inverseImage_equivalence_inverse_eq_map_functor F.asEquivalence, map_map,
    P.map_eq_of_iso F.asEquivalence.counitIso, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v_1, u_1} D
inst_2 : P.RespectsIso
F : Functor.{v, v_1, u, u_1} C D
inst_3 : F.IsEquivalence
erw : (P.map F.asEquivalence.inverse).map F = P
erw₁ : P.map (F.asEquivalence.inverse ⋙ F) = P
erw₂ : P.map (𝟭 D) = P
⊢ (P.inverseImage F).map F = P
have erw₃ : P = P
Tactic: erw [P.inverseImage_equivalence_inverse_eq_map_functor F.asEquivalence, map_map,
    P.map_eq_of_iso F.asEquivalence.counitIso, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
inst_2 : P.RespectsIso
F : Functor.{v, v_1, u, u_1} C D
inst_3 : F.IsEquivalence
⊢ (P.map F).inverseImage F = P
have erw : (P.map F).map F.asEquivalence.inverse = P
Tactic: erw [((P.map F).inverseImage_equivalence_inverse_eq_map_functor (F.asEquivalence)), map_map,
    P.map_eq_of_iso F.asEquivalence.unitIso.symm, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
inst_2 : P.RespectsIso
F : Functor.{v, v_1, u, u_1} C D
inst_3 : F.IsEquivalence
erw : (P.map F).map F.asEquivalence.inverse = P
⊢ (P.map F).inverseImage F = P
have erw₁ : P.map (F ⋙ F.asEquivalence.inverse) = P
Tactic: erw [((P.map F).inverseImage_equivalence_inverse_eq_map_functor (F.asEquivalence)), map_map,
    P.map_eq_of_iso F.asEquivalence.unitIso.symm, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
inst_2 : P.RespectsIso
F : Functor.{v, v_1, u, u_1} C D
inst_3 : F.IsEquivalence
erw : (P.map F).map F.asEquivalence.inverse = P
erw₁ : P.map (F ⋙ F.asEquivalence.inverse) = P
⊢ (P.map F).inverseImage F = P
have erw₂ : P.map (𝟭 C) = P
Tactic: erw [((P.map F).inverseImage_equivalence_inverse_eq_map_functor (F.asEquivalence)), map_map,
    P.map_eq_of_iso F.asEquivalence.unitIso.symm, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
inst_2 : P.RespectsIso
F : Functor.{v, v_1, u, u_1} C D
inst_3 : F.IsEquivalence
erw : (P.map F).map F.asEquivalence.inverse = P
erw₁ : P.map (F ⋙ F.asEquivalence.inverse) = P
erw₂ : P.map (𝟭 C) = P
⊢ (P.map F).inverseImage F = P
have erw₃ : P = P
Tactic: erw [((P.map F).inverseImage_equivalence_inverse_eq_map_functor (F.asEquivalence)), map_map,
    P.map_eq_of_iso F.asEquivalence.unitIso.symm, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ RespectsIso.{v, u} (MorphismProperty.monomorphisms C)
have hprecomp : ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (e.hom ≫ f)
Tactic: apply RespectsIso.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
hprecomp :
  ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z),
    MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (e.hom ≫ f)
⊢ RespectsIso.{v, u} (MorphismProperty.monomorphisms C)
have hpostcomp : ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (f ≫ e.hom)
Tactic: apply RespectsIso.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ RespectsIso.{v, u} (MorphismProperty.epimorphisms C)
have hprecomp : ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (e.hom ≫ f)
Tactic: apply RespectsIso.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
hprecomp :
  ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (e.hom ≫ f)
⊢ RespectsIso.{v, u} (MorphismProperty.epimorphisms C)
have hpostcomp : ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (f ≫ e.hom)
Tactic: apply RespectsIso.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ RespectsIso.{v, u} (MorphismProperty.isomorphisms C)
have hprecomp : ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (e.hom ≫ f)
Tactic: apply RespectsIso.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
hprecomp :
  ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (e.hom ≫ f)
⊢ RespectsIso.{v, u} (MorphismProperty.isomorphisms C)
have hpostcomp : ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (f ≫ e.hom)
Tactic: apply RespectsIso.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
W : MorphismProperty.{v_3, u_3} T
X_1 : T
inst_3 : W.RespectsIso
X Y : Comma L R
e : X ≅ Y
h : commaObj L R W X
⊢ commaObj L R W Y
have rwa : W Y.hom
Tactic: rwa [commaObj_iff, ← W.cancel_left_of_respectsIso (L.map e.hom.left), e.hom.w,
      W.cancel_right_of_respectsIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
W : MorphismProperty.{v_3, u_3} T
X_1 : T
inst_3 : W.RespectsIso
X Y : Comma L R
e : X ≅ Y
h : commaObj L R W X
rwa : W Y.hom
⊢ commaObj L R W Y
have rwa₁ : W (L.map e.hom.left ≫ Y.hom)
Tactic: rwa [commaObj_iff, ← W.cancel_left_of_respectsIso (L.map e.hom.left), e.hom.w,
      W.cancel_right_of_respectsIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
W : MorphismProperty.{v_3, u_3} T
X_1 : T
inst_3 : W.RespectsIso
X Y : Comma L R
e : X ≅ Y
h : commaObj L R W X
rwa : W Y.hom
rwa₁ : W (L.map e.hom.left ≫ Y.hom)
⊢ commaObj L R W Y
have rwa₂ : W (X.hom ≫ R.map e.hom.right)
Tactic: rwa [commaObj_iff, ← W.cancel_left_of_respectsIso (L.map e.hom.left), e.hom.w,
      W.cancel_right_of_respectsIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
W : MorphismProperty.{v_3, u_3} T
X_1 : T
inst_3 : W.RespectsIso
X Y : Comma L R
e : X ≅ Y
h : commaObj L R W X
rwa : W Y.hom
rwa₁ : W (L.map e.hom.left ≫ Y.hom)
rwa₂ : W (X.hom ≫ R.map e.hom.right)
⊢ commaObj L R W Y
have rwa₃ : W X.hom
Tactic: rwa [commaObj_iff, ← W.cancel_left_of_respectsIso (L.map e.hom.left), e.hom.w,
      W.cancel_right_of_respectsIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
inst_5 : Q.RespectsIso
inst_6 : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma (P := P) (Q := Q) (W := W) ⟶ Y.toComma (P := P) (Q := Q) (W := W)
inst_7 : IsIso i
⊢ IsIso (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i)
have out : ∃ (inv : Y ⟶ X),
  homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i ≫ inv = 𝟙 X ∧
    inv ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i = 𝟙 Y
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
inst_5 : Q.RespectsIso
inst_6 : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma (P := P) (Q := Q) (W := W) ⟶ Y.toComma (P := P) (Q := Q) (W := W)
inst_7 : IsIso i
⊢ ∃ (inv : Y ⟶ X),
    homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i ≫ inv = 𝟙 X ∧
      inv ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i = 𝟙 Y
have h : Eq (α := X ⟶ X)
    (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i)) (𝟙 X) ∧
  Eq (α := Y ⟶ Y)
    (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i) ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i) (𝟙 Y)
Tactic: use homFromCommaOfIsIso (inv i)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
inst_5 : Q.RespectsIso
inst_6 : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma (P := P) (Q := Q) (W := W) ⟶ Y.toComma (P := P) (Q := Q) (W := W)
inst_7 : IsIso i
⊢ Eq (α := X ⟶ X)
      (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i))
      (𝟙 X) ∧
    Eq (α := Y ⟶ Y)
      (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i) ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i) (𝟙 Y)
have h : Eq (α := X ⟶ X)
  (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i)) (𝟙 X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
inst_5 : Q.RespectsIso
inst_6 : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma (P := P) (Q := Q) (W := W) ⟶ Y.toComma (P := P) (Q := Q) (W := W)
inst_7 : IsIso i
h :
  Eq (α := X ⟶ X)
    (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i)) (𝟙 X)
⊢ Eq (α := X ⟶ X)
      (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i))
      (𝟙 X) ∧
    Eq (α := Y ⟶ Y)
      (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i) ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i) (𝟙 Y)
have h₁ : Eq (α := Y ⟶ Y)
  (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i) ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i) (𝟙 Y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
inst_5 : Q.RespectsIso
inst_6 : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma (P := P) (Q := Q) (W := W) ⟶ Y.toComma (P := P) (Q := Q) (W := W)
inst_7 : IsIso i
⊢ Eq (α := X ⟶ X)
    (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i)) (𝟙 X)
have h : Hom.hom (P := P) (Q := Q) (W := W)
    (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i)) =
  Hom.hom (P := P) (Q := Q) (W := W) (𝟙 X)
Tactic: ext : 1