awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
Goal:
J : Type
inst : Finite J
C : Type u₁
D : Type u₂
inst_1 : Category.{v₁, u₁} C
inst_2 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : W.ContainsIdentities
inst_4 : L.IsLocalization W
E : J → C ≌ Functor.{0, v₁, 0, u₁} (Discrete J) C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Functor.{0, v₂, 0, u₂} (Discrete J) D := piEquivalenceFunctorDiscrete J D
L₂ : Functor.{0, v₁, 0, u₁} (Discrete J) C ⥤ Functor.{0, v₂, 0, u₂} (Discrete J) D :=
  obj (whiskeringRight (Discrete J) C D) L
L₁ : Functor.{v₁, v₂, u₁, u₂} ((i : J) → C) ((i : J) → D) :=
  Functor.pi (C := fun (x : J) ↦ C) (D := fun (x : J) ↦ D) fun (x : J) ↦ L
this : CatCommSq E.functor L₁ L₂ E'.functor
refine_1 :
  (MorphismProperty.pi (C := fun (i : J) ↦ C) fun (x : J) ↦ W) ≤
    MorphismProperty.inverseImage (MorphismProperty.isoClosure (W.functorCategory (Discrete J))) E.functor
⊢ IsLocalization (C := Functor.{0, v₁, 0, u₁} (Discrete J) C) (obj (whiskeringRight (Discrete J) C D) L)
    (W.functorCategory (Discrete J))
have refine_2 : MorphismProperty.IsInvertedBy (W.functorCategory (Discrete J)) L₂
Tactic: refine Functor.IsLocalization.of_equivalences L₁
    (MorphismProperty.pi (fun _ => W)) L₂ _ E E' ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (hypothesis)
Goal:
J : Type
inst : Finite J
C : Type u₁
D : Type u₂
inst_1 : Category.{v₁, u₁} C
inst_2 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : W.ContainsIdentities
inst_4 : L.IsLocalization W
E : J → C ≌ Functor.{0, v₁, 0, u₁} (Discrete J) C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Functor.{0, v₂, 0, u₂} (Discrete J) D := piEquivalenceFunctorDiscrete J D
L₂ : Functor.{0, v₁, 0, u₁} (Discrete J) C ⥤ Functor.{0, v₂, 0, u₂} (Discrete J) D :=
  obj (whiskeringRight (Discrete J) C D) L
L₁ : Functor.{v₁, v₂, u₁, u₂} ((i : J) → C) ((i : J) → D) :=
  Functor.pi (C := fun (x : J) ↦ C) (D := fun (x : J) ↦ D) fun (x : J) ↦ L
this : CatCommSq E.functor L₁ L₂ E'.functor
X Y : Functor.{0, v₁, 0, u₁} (Discrete J) C
f : X ⟶ Y
hf : W.functorCategory (Discrete J) f
⊢ IsIso (L₂.map f)
have this₁ : ∀ (j : Discrete J), IsIso ((L₂.map f).app j)
Tactic: have : ∀ (j : Discrete J), IsIso ((L₂.map f).app j) :=
      fun j => Localization.inverts L W _ (hf j)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
this : Localization.Construction.lift (W := W) W.Q ⋯ = 𝟭 W.Localization
⊢ (Localization.Construction.lift (W := W) W.Q ⋯).IsEquivalence
have rw : IsEquivalence (C := W.Localization) (𝟭 W.Localization)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
⊢ (Localization.Construction.lift (W := W) W.Q ⋯).IsEquivalence
have suffices : Localization.Construction.lift (W := W) W.Q sorry = 𝟭 W.Localization
Tactic: suffices Localization.Construction.lift W.Q W.Q_inverts = 𝟭 _ by
      rw [this]
      infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
⊢ Localization.Construction.lift (W := W) W.Q ⋯ = 𝟭 W.Localization
have h : W.Q ⋙ Localization.Construction.lift (W := W) W.Q sorry = W.Q ⋙ 𝟭 W.Localization
Tactic: apply Localization.Construction.uniq
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
⊢ W.Q ⋙ Localization.Construction.lift (W := W) W.Q ⋯ = W.Q ⋙ 𝟭 W.Localization
have h : W.Q = W.Q ⋙ 𝟭 W.Localization
Tactic: simp only [Localization.Construction.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
hW : W ≤ MorphismProperty.isomorphisms C
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
⊢ 𝟭 C ⋙ F = F
have mk : ∀ (obj : C → E) (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X))
  (map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g)
  (hF :
    W.IsInvertedBy
      { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E }),
  𝟭 C ⋙ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } =
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp }
Tactic: cases F
Cleared hypotheses: F, hF
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
hW : W ≤ MorphismProperty.isomorphisms C
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} C E
eq : 𝟭 C ⋙ F₁ = 𝟭 C ⋙ F₂
⊢ F₁ = F₂
have mk : ∀ (obj : C → E) (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X))
  (map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g)
  (eq :
    𝟭 C ⋙ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } =
      𝟭 C ⋙ F₂),
  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } = F₂
Tactic: cases F₁
Cleared hypotheses: F₁, eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
hW : W ≤ MorphismProperty.isomorphisms C
F₂ : Functor.{v_1, v_3, u_1, u_3} C E
obj : C → E
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
eq :
  𝟭 C ⋙ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } =
    𝟭 C ⋙ F₂
⊢ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } = F₂
have mk : ∀ (obj_1 : C → E) (map_1 : {X Y : C} → (X ⟶ Y) → (obj_1 X ⟶ obj_1 Y)) (map_id_1 : ∀ (X : C), map_1 (𝟙 X) = 𝟙 (obj_1 X))
  (map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g)
  (eq :
    𝟭 C ⋙ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } =
      𝟭 C ⋙
        { obj := obj_1, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 :
          Functor.{v_1, v_3, u_1, u_3} C E }),
  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v_1, v_3, u_1, u_3} C E } =
    { obj := obj_1, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 }
Tactic: cases F₂
Cleared hypotheses: F₂, eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
X : C
hX : W (𝟙 X)
⊢ (isoOfHom L W (𝟙 X) hX).inv = 𝟙 (L.obj X)
have rw : (isoOfHom L W (𝟙 X) hX).inv ≫ (isoOfHom L W (𝟙 X) hX).hom = 𝟙 (L.obj X) ≫ (isoOfHom L W (𝟙 X) hX).hom
Tactic: rw [← cancel_mono (isoOfHom L W (𝟙 X) hX).hom, Iso.inv_hom_id, id_comp,
    isoOfHom_hom, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
X : C
hX : W (𝟙 X)
rw : (isoOfHom L W (𝟙 X) hX).inv ≫ (isoOfHom L W (𝟙 X) hX).hom = 𝟙 (L.obj X) ≫ (isoOfHom L W (𝟙 X) hX).hom
⊢ (isoOfHom L W (𝟙 X) hX).inv = 𝟙 (L.obj X)
have rw₁ : 𝟙 (L.obj X) = 𝟙 (L.obj X) ≫ (isoOfHom L W (𝟙 X) hX).hom
Tactic: rw [← cancel_mono (isoOfHom L W (𝟙 X) hX).hom, Iso.inv_hom_id, id_comp,
    isoOfHom_hom, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
X : C
hX : W (𝟙 X)
rw : (isoOfHom L W (𝟙 X) hX).inv ≫ (isoOfHom L W (𝟙 X) hX).hom = 𝟙 (L.obj X) ≫ (isoOfHom L W (𝟙 X) hX).hom
rw₁ : 𝟙 (L.obj X) = 𝟙 (L.obj X) ≫ (isoOfHom L W (𝟙 X) hX).hom
⊢ (isoOfHom L W (𝟙 X) hX).inv = 𝟙 (L.obj X)
have rw₂ : 𝟙 (L.obj X) = (isoOfHom L W (𝟙 X) hX).hom
Tactic: rw [← cancel_mono (isoOfHom L W (𝟙 X) hX).hom, Iso.inv_hom_id, id_comp,
    isoOfHom_hom, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
X : C
hX : W (𝟙 X)
rw : (isoOfHom L W (𝟙 X) hX).inv ≫ (isoOfHom L W (𝟙 X) hX).hom = 𝟙 (L.obj X) ≫ (isoOfHom L W (𝟙 X) hX).hom
rw₁ : 𝟙 (L.obj X) = 𝟙 (L.obj X) ≫ (isoOfHom L W (𝟙 X) hX).hom
rw₂ : 𝟙 (L.obj X) = (isoOfHom L W (𝟙 X) hX).hom
⊢ (isoOfHom L W (𝟙 X) hX).inv = 𝟙 (L.obj X)
have rw₃ : 𝟙 (L.obj X) = L.map (𝟙 X)
Tactic: rw [← cancel_mono (isoOfHom L W (𝟙 X) hX).hom, Iso.inv_hom_id, id_comp,
    isoOfHom_hom, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
X : C
hX : W (𝟙 X)
rw : (isoOfHom L W (𝟙 X) hX).inv ≫ (isoOfHom L W (𝟙 X) hX).hom = 𝟙 (L.obj X) ≫ (isoOfHom L W (𝟙 X) hX).hom
rw₁ : 𝟙 (L.obj X) = 𝟙 (L.obj X) ≫ (isoOfHom L W (𝟙 X) hX).hom
rw₂ : 𝟙 (L.obj X) = (isoOfHom L W (𝟙 X) hX).hom
rw₃ : 𝟙 (L.obj X) = L.map (𝟙 X)
⊢ (isoOfHom L W (𝟙 X) hX).inv = 𝟙 (L.obj X)
have rw₄ : Eq.{v_2 + 1} (α := L.obj X ⟶ L.obj X) (𝟙 (L.obj X)) (𝟙 (L.obj X))
Tactic: rw [← cancel_mono (isoOfHom L W (𝟙 X) hX).hom, Iso.inv_hom_id, id_comp,
    isoOfHom_hom, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : W f
⊢ wIso (W := W) f hf = isoOfHom W.Q W f hf
have w : (wIso (W := W) f hf).hom = (isoOfHom W.Q W f hf).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
F : Functor.{v_2, v_3, u_2, u_3} D E
⊢ obj
      (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
        Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
      F =
    obj (whiskeringLeftFunctor L W E) F
have h : (obj
        (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
          Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
        F).obj
    (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F) =
  (obj (whiskeringLeftFunctor L W E) F).obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
F : Functor.{v_2, v_3, u_2, u_3} D E
⊢ (obj
          (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
            Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
          F).obj
      (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F) =
    (obj (whiskeringLeftFunctor L W E) F).obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F)
have h : (W.Q ⋙ Construction.lift (W := W) L sorry) ⋙ F = L ⋙ F
Tactic: change (W.Q ⋙ Localization.Construction.lift L (inverts L W)) ⋙ F = L ⋙ F
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
F : Functor.{v_2, v_3, u_2, u_3} D E
⊢ (W.Q ⋙ Construction.lift (W := W) L ⋯) ⋙ F = L ⋙ F
have h : L ⋙ F = L ⋙ F
Tactic: rw [Construction.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
X Y : Functor.{v_2, v_3, u_2, u_3} D E
τ : X ⟶ Y
x : C
⊢ Eq (α :=
    (obj
                (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
                  Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
                X).obj
            (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
        x ⟶
      (obj (whiskeringLeftFunctor L W E) Y).obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
        x)
    (NatTrans.app
      (InducedCategory.Hom.hom
        (map
            (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
              Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
            τ ≫
          Iso.hom
            ((fun (F : Functor.{v_2, v_3, u_2, u_3} D E) ↦
                (eqToIso ⋯ :
                  obj
                      (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
                        Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
                      F ≅
                    obj (whiskeringLeftFunctor L W E) F))
              Y)))
      x)
    (NatTrans.app
      (InducedCategory.Hom.hom
        (Iso.hom
            ((fun (F : Functor.{v_2, v_3, u_2, u_3} D E) ↦
                (eqToIso ⋯ :
                  obj
                      (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
                        Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
                      F ≅
                    obj (whiskeringLeftFunctor L W E) F))
              X) ≫
          map (whiskeringLeftFunctor L W E) τ))
      x)
have h : Eq (α :=
  X.obj (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ⟶
    (obj (whiskeringLeftFunctor L W E) Y).obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
      x)
  (τ.app (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ≫
    NatTrans.app (InducedCategory.Hom.hom (eqToHom sorry)) x)
  (NatTrans.app (InducedCategory.Hom.hom (eqToHom sorry)) x ≫
    NatTrans.app (InducedCategory.Hom.hom (map (whiskeringLeftFunctor L W E) τ)) x)
Tactic: dsimp [Construction.whiskeringLeftEquivalence, equivalenceFromModel, whiskerLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
X Y : Functor.{v_2, v_3, u_2, u_3} D E
τ : X ⟶ Y
x : C
⊢ Eq (α :=
    X.obj (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ⟶
      (obj (whiskeringLeftFunctor L W E) Y).obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
        x)
    (τ.app (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ≫
      NatTrans.app (InducedCategory.Hom.hom (eqToHom ⋯)) x)
    (NatTrans.app (InducedCategory.Hom.hom (eqToHom ⋯)) x ≫
      NatTrans.app (InducedCategory.Hom.hom (map (whiskeringLeftFunctor L W E) τ)) x)
have h : τ.app (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ≫
    𝟙
      ((obj (Construction.WhiskeringLeftEquivalence.functor W E) (Construction.lift (W := W) L sorry ⋙ Y)).obj (P :=
            fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
        x) =
  𝟙
      ((obj (Construction.WhiskeringLeftEquivalence.functor W E) (Construction.lift (W := W) L sorry ⋙ X)).obj (P :=
            fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
        x) ≫
    NatTrans.app (InducedCategory.Hom.hom (map (whiskeringLeftFunctor L W E) τ)) x
Tactic: rw [ObjectProperty.eqToHom_hom, ObjectProperty.eqToHom_hom, eqToHom_app, eqToHom_app,
          eqToHom_refl, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
X Y : Functor.{v_2, v_3, u_2, u_3} D E
τ : X ⟶ Y
x : C
⊢ τ.app (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ≫
      𝟙
        ((obj (Construction.WhiskeringLeftEquivalence.functor W E) (Construction.lift (W := W) L ⋯ ⋙ Y)).obj (P :=
              fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
          x) =
    𝟙
        ((obj (Construction.WhiskeringLeftEquivalence.functor W E) (Construction.lift (W := W) L ⋯ ⋙ X)).obj (P :=
              fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
          x) ≫
      NatTrans.app (InducedCategory.Hom.hom (map (whiskeringLeftFunctor L W E) τ)) x
have h : τ.app (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ≫
    𝟙 (Y.obj (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W)))) =
  𝟙 (X.obj (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W)))) ≫
    NatTrans.app (InducedCategory.Hom.hom (map (whiskeringLeftFunctor L W E) τ)) x
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
X Y : Functor.{v_2, v_3, u_2, u_3} D E
τ : X ⟶ Y
x : C
⊢ τ.app (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ≫
      𝟙 (Y.obj (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W)))) =
    𝟙 (X.obj (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W)))) ≫
      NatTrans.app (InducedCategory.Hom.hom (map (whiskeringLeftFunctor L W E) τ)) x
have h : Eq (α :=
  X.obj (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))) ⟶
    (obj (whiskeringLeftFunctor L W E) Y).obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
      x)
  (τ.app (L.obj ((W.Q.obj x).as (r := Construction.relations W).obj (W := W))))
  (NatTrans.app (InducedCategory.Hom.hom (map (whiskeringLeftFunctor L W E) τ)) x)
Tactic: rw [comp_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
⊢ Full (C := Functor.{v_2, v_3, u_2, u_3} D E)
    (whiskeringLeftFunctor L W E ⋙
      inducedFunctor
        (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F)))
have apply : Full (C := Functor.{v_2, v_3, u_2, u_3} D E) (whiskeringLeftFunctor L W E)
Tactic: apply @Functor.Full.comp _ _ _ _ _ _ _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
apply : Full (C := Functor.{v_2, v_3, u_2, u_3} D E) (whiskeringLeftFunctor L W E)
⊢ Full (C := Functor.{v_2, v_3, u_2, u_3} D E)
    (whiskeringLeftFunctor L W E ⋙
      inducedFunctor
        (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F)))
have apply₁ : Full (C := MorphismProperty.FunctorsInverting.{v_1, u_1, v_3, u_3} W E)
  (inducedFunctor
    (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F)))
Tactic: apply @Functor.Full.comp _ _ _ _ _ _ _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
⊢ Faithful (C := Functor.{v_2, v_3, u_2, u_3} D E)
    (whiskeringLeftFunctor L W E ⋙
      inducedFunctor
        (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F)))
have apply : Faithful (C := Functor.{v_2, v_3, u_2, u_3} D E) (whiskeringLeftFunctor L W E)
Tactic: apply @Functor.Faithful.comp _ _ _ _ _ _ _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
apply : Faithful (C := Functor.{v_2, v_3, u_2, u_3} D E) (whiskeringLeftFunctor L W E)
⊢ Faithful (C := Functor.{v_2, v_3, u_2, u_3} D E)
    (whiskeringLeftFunctor L W E ⋙
      inducedFunctor
        (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F)))
have apply₁ : Faithful (C := MorphismProperty.FunctorsInverting.{v_1, u_1, v_3, u_3} W E)
  (inducedFunctor
    (ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F)))
Tactic: apply @Functor.Faithful.comp _ _ _ _ _ _ _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L_1 : Functor.{v_1, v_2, u_1, u_2} C D
W_1 : MorphismProperty.{v_1, u_1} C
E_1 : Type u_3
inst_2 : Category.{v_3, u_3} E_1
inst_3 : L_1.IsLocalization W_1
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_4 : L.IsLocalization W
E : Type u_4
inst_5 : Category.{v_4, u_4} E
⊢ FullyFaithful (C := Functor.{v_2, v_4, u_2, u_4} D E) (obj (whiskeringLeft C D E) L)
have this : Full (C := Functor.{v_2, v_4, u_2, u_4} D E) (obj (whiskeringLeft C D E) L)
Tactic: have := full_whiskeringLeft L W E