awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
α : Type
inst_3 : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
inst_4 : EffectiveEpiFamily X π
⊢ EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)

Tactic:
PreservesFiniteEffectiveEpiFamilies.preserves X π

Premises used: CategoryTheory.Functor.PreservesFiniteEffectiveEpiFamilies.preserves
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.PreservesEffectiveEpis
inst_4 : G.PreservesEffectiveEpis
X Y : C
x : X ⟶ Y
h : EffectiveEpi x
dsimp : EffectiveEpi (G.map (F.map x))
⊢ EffectiveEpi ((F ⋙ G).map x)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.PreservesEffectiveEpis
inst_4 : G.PreservesEffectiveEpis
X Y : C
x : X ⟶ Y
h : EffectiveEpi x
⊢ EffectiveEpi (G.map (F.map x))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.PreservesFiniteEffectiveEpiFamilies
inst_4 : G.PreservesFiniteEffectiveEpiFamilies
α : Type
inst_5 : Finite α
B : C
x : α → C
x_1 : (a : α) → x a ⟶ B
h : EffectiveEpiFamily x x_1
dsimp :
  EffectiveEpiFamily.{v_3, u_3, 0} (C := E) (B := G.obj (F.obj B)) (fun (a : α) ↦ G.obj (F.obj (x a))) fun (a : α) ↦
    G.map (F.map (x_1 a))
⊢ EffectiveEpiFamily.{v_3, u_3, 0} (C := E) (B := (F ⋙ G).obj B) (fun (a : α) ↦ (F ⋙ G).obj (x a)) fun (a : α) ↦
    (F ⋙ G).map (x_1 a)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.PreservesFiniteEffectiveEpiFamilies
inst_4 : G.PreservesFiniteEffectiveEpiFamilies
α : Type
inst_5 : Finite α
B : C
x : α → C
x_1 : (a : α) → x a ⟶ B
h : EffectiveEpiFamily x x_1
⊢ EffectiveEpiFamily.{v_3, u_3, 0} (C := E) (B := G.obj (F.obj B)) (fun (a : α) ↦ G.obj (F.obj (x a))) fun (a : α) ↦
    G.map (F.map (x_1 a))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.PreservesEffectiveEpiFamilies
inst_4 : G.PreservesEffectiveEpiFamilies
α : Type u
B : C
x : α → C
x_1 : (a : α) → x a ⟶ B
h : EffectiveEpiFamily x x_1
dsimp :
  EffectiveEpiFamily.{v_3, u_3, u} (C := E) (B := G.obj (F.obj B)) (fun (a : α) ↦ G.obj (F.obj (x a))) fun (a : α) ↦
    G.map (F.map (x_1 a))
⊢ EffectiveEpiFamily.{v_3, u_3, u} (C := E) (B := (F ⋙ G).obj B) (fun (a : α) ↦ (F ⋙ G).obj (x a)) fun (a : α) ↦
    (F ⋙ G).map (x_1 a)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.PreservesEffectiveEpiFamilies
inst_4 : G.PreservesEffectiveEpiFamilies
α : Type u
B : C
x : α → C
x_1 : (a : α) → x a ⟶ B
h : EffectiveEpiFamily x x_1
⊢ EffectiveEpiFamily.{v_3, u_3, u} (C := E) (B := G.obj (F.obj B)) (fun (a : α) ↦ G.obj (F.obj (x a))) fun (a : α) ↦
    G.map (F.map (x_1 a))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.ReflectsEffectiveEpis
X Y : C
f : X ⟶ Y
h : EffectiveEpi (F.map f)
⊢ EffectiveEpi f

Tactic:
ReflectsEffectiveEpis.reflects f h

Premises used: CategoryTheory.Functor.ReflectsEffectiveEpis.reflects
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.ReflectsEffectiveEpiFamilies
α : Type u
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, u} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)
⊢ EffectiveEpiFamily X π

Tactic:
ReflectsEffectiveEpiFamilies.reflects X π h

Premises used: CategoryTheory.Functor.ReflectsEffectiveEpiFamilies.reflects
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.ReflectsFiniteEffectiveEpiFamilies
α : Type
inst_3 : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)
⊢ EffectiveEpiFamily X π

Tactic:
ReflectsFiniteEffectiveEpiFamilies.reflects X π h

Premises used: CategoryTheory.Functor.ReflectsFiniteEffectiveEpiFamilies.reflects
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.ReflectsEffectiveEpiFamilies
α : Type
inst_3 : Finite α
B : C
x : α → C
x_1 : (a : α) → x a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (x a)) fun (a : α) ↦ F.map (x_1 a)
⊢ EffectiveEpiFamily x x_1

Tactic:
have := F.effectiveEpiFamily_of_map _ _ h
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.ReflectsEffectiveEpiFamilies
α : Type
inst_3 : Finite α
B : C
x : α → C
x_1 : (a : α) → x a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (x a)) fun (a : α) ↦ F.map (x_1 a)
this : EffectiveEpiFamily x x_1
⊢ EffectiveEpiFamily x x_1

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.ReflectsFiniteEffectiveEpiFamilies
X Y : C
x : X ⟶ Y
h : EffectiveEpi (F.map x)
⊢ EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj Y) (fun (x : Unit) ↦ F.obj X) fun (x_1 : Unit) ↦
    match (motive := (x : Unit) → (fun (x : Unit) ↦ F.obj X) x ⟶ F.obj Y) x_1 with
    | PUnit.unit => F.map x

Tactic:
rw [effectiveEpi_iff_effectiveEpiFamily] at h

Premises used: CategoryTheory.effectiveEpi_iff_effectiveEpiFamily
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.ReflectsFiniteEffectiveEpiFamilies
X Y : C
x : X ⟶ Y
h :
  EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj Y) (fun (x : Unit) ↦ F.obj X) fun (x_1 : Unit) ↦
    match (motive := (x : Unit) → (fun (x : Unit) ↦ F.obj X) x ⟶ F.obj Y) x_1 with
    | PUnit.unit => F.map x
⊢ EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := Y) (fun (a : Unit) ↦ X) fun (a : Unit) ↦ x

Tactic:
have := F.finite_effectiveEpiFamily_of_map _ _ h
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.ReflectsFiniteEffectiveEpiFamilies
X Y : C
x : X ⟶ Y
h :
  EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj Y) (fun (x : Unit) ↦ F.obj X) fun (x_1 : Unit) ↦
    match (motive := (x : Unit) → (fun (x : Unit) ↦ F.obj X) x ⟶ F.obj Y) x_1 with
    | PUnit.unit => F.map x
this : EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := Y) (fun (a : Unit) ↦ X) fun (a : Unit) ↦ x
⊢ EffectiveEpi x

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.IsEquivalence
α : Type u_3
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, u_3} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)
i : (a : α) → X a ⟶ F.inv.obj (F.obj (X a)) := fun (a : α) ↦ F.asEquivalence.unit.app (X a)
⊢ EffectiveEpiFamily.{v_1, u_1, u_3} (B := F.inv.obj (F.obj B)) X fun (a : α) ↦ i a ≫ F.inv.map (F.map (π a))

Tactic:
have : EffectiveEpiFamily X (fun a ↦ (i a) ≫ (inv F).map (F.map (π a))) := inferInstance
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.IsEquivalence
α : Type u_3
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, u_3} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)
i : (a : α) → X a ⟶ F.inv.obj (F.obj (X a)) := fun (a : α) ↦ F.asEquivalence.unit.app (X a)
this : EffectiveEpiFamily.{v_1, u_1, u_3} (B := F.inv.obj (F.obj B)) X fun (a : α) ↦ i a ≫ F.inv.map (F.map (π a))
⊢ EffectiveEpiFamily.{v_1, u_1, u_3} (B := F.inv.obj (F.obj B)) X fun (a : α) ↦ π a ≫ F.asEquivalence.unit.app B

Tactic:
simp only [inv_fun_map, Iso.hom_inv_id_app_assoc, i] at this

Premises used: CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.Functor.inv_fun_map
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.IsEquivalence
α : Type u_3
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, u_3} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)
i : (a : α) → X a ⟶ F.inv.obj (F.obj (X a)) := fun (a : α) ↦ F.asEquivalence.unit.app (X a)
this : EffectiveEpiFamily.{v_1, u_1, u_3} (B := F.inv.obj (F.obj B)) X fun (a : α) ↦ π a ≫ F.asEquivalence.unit.app B
⊢ EffectiveEpiFamily.{v_1, u_1, u_3} (B := obj.{v_1, v_1, u_1, u_1} (𝟭 C) B) X fun (a : α) ↦
    (π a ≫ F.asEquivalence.unit.app B) ≫ F.asEquivalence.unitInv.app B

Tactic:
have : EffectiveEpiFamily X (fun a ↦ (π a ≫ (asEquivalence F).unit.app B) ≫
        (asEquivalence F).unitInv.app _) := inferInstance
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.IsEquivalence
α : Type u_3
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, u_3} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)
i : (a : α) → X a ⟶ F.inv.obj (F.obj (X a)) := fun (a : α) ↦ F.asEquivalence.unit.app (X a)
this_1 : EffectiveEpiFamily.{v_1, u_1, u_3} (B := F.inv.obj (F.obj B)) X fun (a : α) ↦ π a ≫ F.asEquivalence.unit.app B
this :
  EffectiveEpiFamily.{v_1, u_1, u_3} (B := obj.{v_1, v_1, u_1, u_1} (𝟭 C) B) X fun (a : α) ↦
    (π a ≫ F.asEquivalence.unit.app B) ≫ F.asEquivalence.unitInv.app B
⊢ EffectiveEpiFamily X π

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
x y : F.Elements
h₁ : x.fst (β := fun (c : C) ↦ F.obj c) = y.fst (β := fun (c : C) ↦ F.obj c)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom h₁)) :
        (a : (fun (X : Type w) ↦ X) (F.obj x.fst)) → (fun (X : Type w) ↦ X) (F.obj y.fst))
      (x.snd (β := fun (c : C) ↦ F.obj c)) =
    y.snd (β := fun (c : C) ↦ F.obj c)
mk :
  ∀ (fst : C) (snd : F.obj fst)
    (h₁ :
      (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).fst (β := fun (c : C) ↦ F.obj c) =
        y.fst (β := fun (c : C) ↦ F.obj c))
    (h₂ :
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom h₁)) :
            (a : (fun (X : Type w) ↦ X) (F.obj ⟨fst, snd⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj y.fst))
          ((Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).snd (β := fun (c : C) ↦ F.obj c)) =
        y.snd (β := fun (c : C) ↦ F.obj c)),
    Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd = y
⊢ x = y

Tactic:
cases x
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
y : F.Elements
fst : C
snd : F.obj fst
h₁ :
  (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).fst (β := fun (c : C) ↦ F.obj c) = y.fst (β := fun (c : C) ↦ F.obj c)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom h₁)) :
        (a : (fun (X : Type w) ↦ X) (F.obj ⟨fst, snd⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj y.fst))
      ((Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).snd (β := fun (c : C) ↦ F.obj c)) =
    y.snd (β := fun (c : C) ↦ F.obj c)
mk :
  ∀ (fst_1 : C) (snd_1 : F.obj fst_1)
    (h₁ :
      (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).fst (β := fun (c : C) ↦ F.obj c) =
        (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst_1 snd_1).fst (β := fun (c : C) ↦ F.obj c))
    (h₂ :
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom h₁)) :
            (a : (fun (X : Type w) ↦ X) (F.obj ⟨fst, snd⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj ⟨fst_1, snd_1⟩.fst))
          ((Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).snd (β := fun (c : C) ↦ F.obj c)) =
        (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst_1 snd_1).snd (β := fun (c : C) ↦ F.obj c)),
    Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd = Sigma.mk (β := fun (c : C) ↦ F.obj c) fst_1 snd_1
⊢ Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd = y

Tactic:
cases y
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
fst : C
snd : F.obj fst
fst_1 : C
snd_1 : F.obj fst_1
h₁ :
  (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).fst (β := fun (c : C) ↦ F.obj c) =
    (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst_1 snd_1).fst (β := fun (c : C) ↦ F.obj c)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom h₁)) :
        (a : (fun (X : Type w) ↦ X) (F.obj ⟨fst, snd⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj ⟨fst_1, snd_1⟩.fst))
      ((Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).snd (β := fun (c : C) ↦ F.obj c)) =
    (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst_1 snd_1).snd (β := fun (c : C) ↦ F.obj c)
mk :
  ∀ (snd_2 : F.obj fst)
    (h₂ :
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom ⋯)) :
            (a : (fun (X : Type w) ↦ X) (F.obj ⟨fst, snd⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj ⟨fst, snd_2⟩.fst))
          ((Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).snd (β := fun (c : C) ↦ F.obj c)) =
        (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd_2).snd (β := fun (c : C) ↦ F.obj c)),
    Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd = Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd_2
⊢ Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd = Sigma.mk (β := fun (c : C) ↦ F.obj c) fst_1 snd_1

Tactic:
cases h₁
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
fst : C
snd snd_1 : F.obj fst
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom ⋯)) :
        (a : (fun (X : Type w) ↦ X) (F.obj ⟨fst, snd⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj ⟨fst, snd_1⟩.fst))
      ((Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).snd (β := fun (c : C) ↦ F.obj c)) =
    (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd_1).snd (β := fun (c : C) ↦ F.obj c)
⊢ Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd = Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd_1

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
p : F.Elements
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 (p.fst (β := fun (c : C) ↦ F.obj c)))) :
        (a : (fun (X : Type w) ↦ X) (F.obj p.fst)) → (fun (X : Type w) ↦ X) (F.obj p.fst))
      (p.snd (β := fun (c : C) ↦ F.obj c)) =
    p.snd (β := fun (c : C) ↦ F.obj c)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X Y Z : F.Elements
f :
  { f : X.fst (β := fun (c : C) ↦ F.obj c) ⟶ Y.fst (β := fun (c : C) ↦ F.obj c) //
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type w) ↦ X) (F.obj X.fst)) → (fun (X : Type w) ↦ X) (F.obj Y.fst))
        (X.snd (β := fun (c : C) ↦ F.obj c)) =
      Y.snd (β := fun (c : C) ↦ F.obj c) }
g :
  { f : Y.fst (β := fun (c : C) ↦ F.obj c) ⟶ Z.fst (β := fun (c : C) ↦ F.obj c) //
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type w) ↦ X) (F.obj Y.fst)) → (fun (X : Type w) ↦ X) (F.obj Z.fst))
        (Y.snd (β := fun (c : C) ↦ F.obj c)) =
      Z.snd (β := fun (c : C) ↦ F.obj c) }
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ((↑f : X.fst ⟶ Y.fst) ≫ (↑g : Y.fst ⟶ Z.fst))) :
        (a : (fun (X : Type w) ↦ X) (F.obj X.fst)) → (fun (X : Type w) ↦ X) (F.obj Z.fst))
      (X.snd (β := fun (c : C) ↦ F.obj c)) =
    Z.snd (β := fun (c : C) ↦ F.obj c)

Tactic:
simp [f.2, g.2]

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
φ : F ⟶ G
p q : F.Elements
x : p ⟶ q
f : p.fst (β := fun (c : C) ↦ F.obj c) ⟶ q.fst (β := fun (c : C) ↦ F.obj c)
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
        (a : (fun (X : Type w) ↦ X) (F.obj p.fst)) → (fun (X : Type w) ↦ X) (F.obj q.fst))
      (p.snd (β := fun (c : C) ↦ F.obj c)) =
    q.snd (β := fun (c : C) ↦ F.obj c)
⊢ Eq (α := G.obj (q.fst (β := fun (c : C) ↦ F.obj c)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app (q.fst (β := fun (c : C) ↦ F.obj c))) :
          (a : F.obj q.fst) → G.obj q.fst)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj p.fst) → F.obj q.fst)
            (p.snd (β := fun (c : C) ↦ F.obj c)) :
          F.obj (q.fst (β := fun (c : C) ↦ F.obj c))) :
      G.obj (q.fst (β := fun (c : C) ↦ F.obj c)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) : (a : G.obj p.fst) → G.obj q.fst)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app (p.fst (β := fun (c : C) ↦ F.obj c))) :
              (a : F.obj p.fst) → G.obj p.fst)
            (p.snd (β := fun (c : C) ↦ F.obj c)) :
          G.obj (p.fst (β := fun (c : C) ↦ F.obj c))) :
      G.obj (q.fst (β := fun (c : C) ↦ F.obj c)))

Tactic:
have hb := φ.naturality_apply f p.2
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
x y : F.Elements
f g : x ⟶ y
w : (↑f : x.fst ⟶ y.fst) = (↑g : x.fst ⟶ y.fst)
⊢ f = g

Tactic:
Subtype.ext w

Premises used: Subtype.ext
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
p q r : F.Elements
f : p ⟶ q
g : q ⟶ r
⊢ (↑(f ≫ g) : p.fst ⟶ r.fst) = (↑f : p.fst ⟶ q.fst) ≫ (↑g : q.fst ⟶ r.fst)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
p : F.Elements
⊢ (↑(𝟙 p) : p.fst ⟶ p.fst) = 𝟙 (p.fst (β := fun (c : C) ↦ F.obj c))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
p q : F.Elements
f : p ⟶ q
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (↑f : p.fst ⟶ q.fst)) :
        (a : (fun (X : Type w) ↦ X) (F.obj p.fst)) → (fun (X : Type w) ↦ X) (F.obj q.fst))
      (p.snd (β := fun (c : C) ↦ F.obj c)) =
    q.snd (β := fun (c : C) ↦ F.obj c)

Tactic:
f.property

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
x y : F.Elements
e : x.fst (β := fun (c : C) ↦ F.obj c) ≅ y.fst (β := fun (c : C) ↦ F.obj c)
he :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom) :
        (a : (fun (X : Type w) ↦ X) (F.obj x.fst)) → (fun (X : Type w) ↦ X) (F.obj y.fst))
      (x.snd (β := fun (c : C) ↦ F.obj c)) =
    y.snd (β := fun (c : C) ↦ F.obj c)
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.inv) :
        (a : (fun (X : Type w) ↦ X) (F.obj y.fst)) → (fun (X : Type w) ↦ X) (F.obj x.fst))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom) :
            (a : (fun (X : Type w) ↦ X) (F.obj x.fst)) → (fun (X : Type w) ↦ X) (F.obj y.fst))
          (x.snd (β := fun (c : C) ↦ F.obj c)) :
        (fun (X : Type w) ↦ X) (F.obj (y.fst (β := fun (c : C) ↦ F.obj c)))) =
    x.snd (β := fun (c : C) ↦ F.obj c)
rw₁ rw₂ : x.snd (β := fun (c : C) ↦ F.obj c) = x.snd (β := fun (c : C) ↦ F.obj c)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.inv) :
        (a : (fun (X : Type w) ↦ X) (F.obj y.fst)) → (fun (X : Type w) ↦ X) (F.obj x.fst))
      (y.snd (β := fun (c : C) ↦ F.obj c)) =
    x.snd (β := fun (c : C) ↦ F.obj c)

Tactic:
rw [← he, Functor.map_hom_inv'_apply]

Premises used: CategoryTheory.Functor.map_hom_inv'_apply
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X : C
snd : F.obj X
Y : C
y : F.obj Y
⊢ Small.{w, v} (Sigma.mk (β := fun (c : C) ↦ F.obj c) X snd ⟶ Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y)

Tactic:
exact small_of_injective (f := fun g ↦ g.val) (by cat_disch)

Premises used: small_of_injective
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u
inst_1 : Groupoid.{v, u} G
F : Functor.{v, w, u, w + 1} G (Type w)
p q : F.Elements
f : p ⟶ q
rw rw₁ :
  Eq (α := (fun (X : Type w) ↦ X) (F.obj (p.fst (β := fun (c : G) ↦ F.obj c))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Groupoid.inv (↑f : p.fst ⟶ q.fst))) :
          (a : (fun (X : Type w) ↦ X) (F.obj q.fst)) → (fun (X : Type w) ↦ X) (F.obj p.fst))
        (q.snd (β := fun (c : G) ↦ F.obj c)) :
      (fun (X : Type w) ↦ X) (F.obj (p.fst (β := fun (c : G) ↦ F.obj c))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Groupoid.inv (↑f : p.fst ⟶ q.fst))) :
          (a : (fun (X : Type w) ↦ X) (F.obj q.fst)) → (fun (X : Type w) ↦ X) (F.obj p.fst))
        (q.snd (β := fun (c : G) ↦ F.obj c)) :
      (fun (X : Type w) ↦ X) (F.obj (p.fst (β := fun (c : G) ↦ F.obj c))))
⊢ Eq (α := (fun (X : Type w) ↦ X) (F.obj (p.fst (β := fun (c : G) ↦ F.obj c))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Groupoid.inv (↑f : p.fst ⟶ q.fst))) :
          (a : (fun (X : Type w) ↦ X) (F.obj q.fst)) → (fun (X : Type w) ↦ X) (F.obj p.fst))
        (q.snd (β := fun (c : G) ↦ F.obj c)) :
      (fun (X : Type w) ↦ X) (F.obj (p.fst (β := fun (c : G) ↦ F.obj c))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Groupoid.inv (↑f : p.fst ⟶ q.fst))) :
          (a : (fun (X : Type w) ↦ X) (F.obj q.fst)) → (fun (X : Type w) ↦ X) (F.obj p.fst))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (↑f : p.fst ⟶ q.fst)) :
              (a : (fun (X : Type w) ↦ X) (F.obj p.fst)) → (fun (X : Type w) ↦ X) (F.obj q.fst))
            (p.snd (β := fun (c : G) ↦ F.obj c)) :
          (fun (X : Type w) ↦ X) (F.obj (q.fst (β := fun (c : G) ↦ F.obj c)))) :
      (fun (X : Type w) ↦ X) (F.obj (p.fst (β := fun (c : G) ↦ F.obj c))))

Tactic:
rw [f.2]

Premises used: Subtype.property